型家庭，GADTs并命名为记录

问题描述：

在下面的代码编译错误，T1和T2编译罚款，但T3失败：型家庭，GADTs并命名为记录

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 

type family F a 

data T1 b where 
    T1 :: a -> T1 (F a) 

data T2 b where 
    T2 :: { x2 :: a } -> T2 a 

data T3 b where 
    T3 :: { x3 :: a } -> T3 (F a)

我试图理解为什么。 T3只是T1但带有一个已命名的记录。这似乎没有那么特别，因为可以使用构造函数语法来提取它。

这些例子可能看起来很愚蠢，但在我的代码中有a的限制，例如， (Show a)，所以这些值可以在提取时使用。

答

让我们忘记T2和T3，并试图为T1定义提取函数。该类型应该是什么？你可能猜到x1 :: T1 (F a) -> a。但是，这是不对的，如果你尝试它，那么你会得到定义T3的同样的错误。

的问题是，如果有人给你一个T1 T，你碰巧知道一个类型A这样F A是T，则不能得出这样的结论T1 T包含A类型的值，因为它可能代替含有另一种类型B与F B等于T。作为一个极端的例子，假设我们有

type instance F _ =()

那么，如果我们把我们的猜测x1 :: T1 (F a) -> a，我们不得不

T1 :: a -> T1() 
x1 :: T1() -> b

和作曲这些将让我们写a -> b，这是不好的。

真正的类型x1是一样的东西存在，提供约束

T1 t -> (exists a. (F a ~ t) *> a)

这GHC不支持。

与T3的问题是有效的，如果你有

data T3' where T3' :: { x3' :: a } -> T3'

可以提取与模式匹配字段（如果有多个字段或约束，这可能是有用的）相同，但与记录选择器或功能。

型家庭，GADTs并命名为记录

相关推荐