使用类型系列,GADT和命名记录编译错误

Question

在下面的代码,T1并T2编译罚款,但T3失败:

{-# 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),因此可以在提取这些值时使用这些值.

Answer 1

让我们忘记T2和T3,并尝试为其定义一个提取函数T1.该类型应该是什么？

x1 :: ???
x1 (T1 a) = a

好吧,你可能猜到了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'

您可以使用模式匹配提取字段(如果有更多字段或约束,这可能很有用),但不能使用记录选择器或函数.