типы Ранг N в LET привязок

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 

И все это, кажется, работает, как ожидалось.

То, с чем я борюсь, - это определение значения Person внутри привязки let. Например, это не работает:

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

Дает мне:

Не удалось соответствовать ожидаемому типу `t1' с фактическим типом` [Char] `t1' неприкасаемых ...

Есть ли способ сделать эту работу внутри связывания?

Answer 1

Вам нужно явные аннотации типа, когда GADTs участвуют:

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, чтобы принять также PersonField Int и вернуть номер. Это связано с ранее выведенным типом, вызывая ошибку типа.

При явной аннотации типа, вывод типа не будет пытаться вывести неправильный тип для x: он был предоставлен пользователем. Вместо этого будет выполняться только проверка типа.