haskell - GADT 或幻像类型对函数调用进行类型检查，但保持类型的同质性

Question

我认为可以使用类型算术解决以下问题，但尚未找到解决方案。

问题

我有一个从字符串到值的有限映射(使用 Tries 作为实现)，我从二进制/文本文件(json、xml、...)中解析该映射。

type Value = ...
type Attributes = Data.Trie Value 
data Object = Object Attributes

每个映射都具有相同类型的值，但不具有相同的键集。我将具有同一组键的 map 分组在一起，以便能够避免一直进行类型切换我有一个需要某些键的专门功能:

data T1
data T2 
...

data Object a where
    T1 :: Attributes -> Object T1
    T2 :: Attributes -> Object T2
    ...

这允许我写一些类似的东西:

f1 :: Object T1 -> ...

而不是

f1 :: Object ->
f1 o | check_if_T1 o = ...

这可行，但有两个缺点:

1. 同类对象列表现在变得异构，即我不能再拥有列表 [Object]。

2. 我需要编写大量样板来获取/设置属性:

   get :: Object a -> Attributes
   get (T1 a) = a
   get (T2 a) = a
   ...
   

问题

1. 是否有更好的方法根据 ADT 的构造函数来专门化函数？

2. 我怎样才能重新获得拥有列表[对象]的能力？是否有专门的 Dynamic 版本只允许某些类型？我考虑过再次包装对象，但这会增加很多样板文件。例如，

   数据 TObject = TT1 T1 | TT2 T2 ...

我需要的是:

get :: a -> TObject -> Object a

这样我就可以得出:

collect :: a -> [TObject] -> [Object a]

我研究了 HList 但我认为它不适合我的问题。特别是，因为 [Object] 中的类型顺序在编译时未知。

在我看来，这可以使用函数依赖/类型算术来解决，但我只是还没有找到一个好的方法。

Answer 1

1. 如果所有构造函数都返回单态 Object 类型并且没有递归，您可能需要考虑仅使用单独的类型。而不是

   data T1
   data T2
   
   data Object a where
       T1 :: Attributes -> Object T1
       T2 :: Attributes -> Object T2
   

   考虑

   data T1 = T1 Attributes
   data T2 = T2 Attributes
   

2. Dynamic 是一种方法，使用上面的方法，您只需添加 deriving Typeable 即可完成。或者，您也可以手动完成:

   data TSomething = It's1 T1 | It's2 T2
   
   getT1s :: [TSomething] -> [T1]
   getT2s :: [TSomething] -> [T2]
   getT1s xs = [t1 | It's1 t1 <- xs]
   getT2s xs = [t2 | It's2 t2 <- xs]
   

   正如您所说，这涉及一些样板文件。 Typeable 版本看起来更好一点:

   deriving Typeable T1
   deriving Typeable T2
   
   -- can specialize at the call-site to
   -- getTs :: [Dynamic] -> [T1] or
   -- getTs :: [Dynamic] -> [T2]
   getTs :: Typeable a => [Dynamic] -> [a]
   getTs xs = [x | Just x <- map fromDynamic xs]