Что означают данные в Haskell?

Я видел этот фрагмент в журнале разработчиков omegagb:

data ExecutionAST result where
  Return :: result -> ExecutionAST result
  Bind :: (ExecutionAST oldres) -> (oldres -> ExecutionAST result) ->
          ExecutionAST result
  WriteRegister :: M_Register -> Word8 -> ExecutionAST ()
  ReadRegister :: M_Register -> ExecutionAST Word8
  WriteRegister2 :: M_Register2 -> Word16 -> ExecutionAST ()
  ReadRegister2 :: M_Register2 -> ExecutionAST Word16
  WriteMemory :: Word16 -> Word8 -> ExecutionAST ()
  ReadMemory :: Word16 -> ExecutionAST Word8

Что означает data ... where? Я думал, что ключевое слово data используется для определения нового типа.


person wliao    schedule 23.11.2011    source источник


Ответы (2)


Он определяет новый тип, синтаксис которого называется обобщенный алгебраический тип данных.

Это более общий синтаксис, чем обычный. Вы можете написать любое определение нормального типа (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
comment
Кто-нибудь может мне объяснить, зачем здесь нужен GADT? - person wliao; 24.11.2011
comment
@wliao: добавлено объяснение. - person sdcvvc; 24.11.2011
comment
Я считаю, что ваше объяснение лучше, чем видеоклип. Спасибо. - person wliao; 24.11.2011

Обратите внимание, что также можно установить ограничения класса:

data E a where
  A :: Eq b => b -> E b
person nponeccop    schedule 23.11.2011
comment
И что более важно, в отличие от обычных объявлений data, это фактически приводит к тому, что словарь экземпляра сохраняется в типе, что позволяет вам восстановить его путем сопоставления с образцом, как и в случае с экзистенциальными типами. - person hammar; 23.11.2011
comment
@hammar Я не понимаю, что означает ваш комментарий. Я не понимаю эту формулировку (с моей перефразировкой) «восстановить словарь экземпляра через сопоставление с образцом, потому что он хранится в типе». Когда я сопоставляю шаблон, я деконструирую в соответствии с формой структуры, и я не понимаю, как это переводится в словарь экземпляра и почему он отличается от того, что он хранится в типе. Что я должен прочитать/выучить, чтобы понять смысл этого? - person Stephane Rolland; 17.06.2018