Что означают данные ... где в Хаскеле? - PullRequest
Новая
       18

Что означают данные ... где в Хаскеле?

46 голосов
/ 23 ноября 2011

Я видел этот фрагмент в в журнале 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 используется для определения нового типа.

Ответы [ 2 ]

58 голосов
/ 23 ноября 2011

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

Он является более общим, чем обычный синтаксис.Вы можете написать любое определение нормального типа (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)

Если выперепутанный, проверьте связанный видео для более простого, связанного примера.

18 голосов
/ 23 ноября 2011

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

data E a where
  A :: Eq b => b -> E b
...