Он определяет новый тип, синтаксис которого называется обобщенный алгебраический тип данных.
Это более общий синтаксис, чем обычный. Вы можете написать любое определение нормального типа (ADT), используя GADT:
data E a = A a | B Integer
можно записать как:
data E a where
A :: a -> E a
B :: Integer -> E a
Но вы также можете ограничить то, что находится справа:
data E a where
A :: a -> E a
B :: Integer -> E a
C :: Bool -> E Bool
что невозможно при обычном объявлении ADT.
Чтобы узнать больше, посетите вики Haskell или это видео.
Причина в безопасности типов. Предполагается, что ExecutionAST t
является типом операторов, возвращающих t
. Если вы пишете обычный ADT
data ExecutionAST result = Return result
| WriteRegister M_Register Word8
| ReadRegister M_Register
| ReadMemory Word16
| WriteMemory Word16
| ...
тогда ReadMemory 5
будет полиморфным значением типа ExecutionAST t
вместо мономорфного ExecutionAST Word8
, и это будет проверка типа:
x :: M_Register2
x = ...
a = Bind (ReadMemory 1) (WriteRegister2 x)
Этот оператор должен читать память из ячейки 1 и записывать в регистр x
. Однако чтение из памяти дает 8-битные слова, а запись в x
требует 16-битных слов. Используя GADT, вы можете быть уверены, что это не скомпилируется. Ошибки времени компиляции лучше, чем ошибки времени выполнения.
GADT также включают экзистенциальные типы. Если вы попытались написать bind таким образом:
data ExecutionAST result = ...
| Bind (ExecutionAST oldres)
(oldres -> ExecutionAST result)
тогда он не будет компилироваться, так как «oldres» не входит в область действия, вам нужно написать:
data ExecutionAST result = ...
| forall oldres. Bind (ExecutionAST oldres)
(oldres -> ExecutionAST result)
Если вы запутались, посмотрите связанное видео для более простого связанного примера.
person
sdcvvc
schedule
23.11.2011