Подтвердить что ты не робот

Что такое данные... где среднее значение в Haskell?

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

Ответ 1

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

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

Причиной является безопасность типа. 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)

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

Ответ 2

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

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