在let绑定中排名N类型

Question

所以我做到了......

{-# LANGUAGE Rank2Types, GADTs  #-}

type Record fields = forall t. fields t -> t

data PersonField t where
    Name :: PersonField String
    Age :: PersonField Int
type Person = Record PersonField

然后......

nigel :: Person
nigel Name = "Nigel"
nigel Age = 39

这一切似乎都按预期工作.

我正在努力的是如何在let绑定中定义Person值.例如,这不起作用:

abigail :: Person
abigail = let x Name = "Abigail"
              x Age = 27 
           in x  

给我:

无法将预期类型`t1'与实际类型匹配`[Char]'`t1'是不可触及的...

有没有办法让这个工作在let绑定中？

Answer 1

涉及GADT时,您需要显式类型注释:

abigail :: Person
abigail = let x :: Person
              x Name = "Abigail"
              x Age = 27 
           in x

没有它,GHC大致看到了

let x Name = "Abigail"

并说"好吧,x是一种功能,从类型Name,即PersonField String类型"Abigail",即String.在下一行,

let x Name = "Abigail"
    x Age = 27

GHC现在发现x也接受a PersonField Int并返回一个数字.这与先前推断的类型冲突,触发类型错误.

使用显式类型注释,类型推断不会尝试推断错误类型x:它是由用户提供的.相反,只会执行类型检查.