новая типоподобная операционная семантика для GADT, где тип полностью определяет конструктор - PullRequest
Новая
       83

новая типоподобная операционная семантика для GADT, где тип полностью определяет конструктор

1 голос
/ 16 февраля 2020

Предположим, у меня есть GADT, подобный следующему: 

data Tag = A | B | C

data Payload (tag :: Tag) where
  PA :: Int -> Payload A
  PB :: Double -> Payload B
  PC :: Bool -> Payload C

Я хочу, чтобы Payload не имел самостоятельного представления во время выполнения - т.е. я хочу иметь Coercible Int (Payload A), я хочу нулевую стоимость сопоставление с образцом, и в целом я хочу, чтобы он вел себя так, как если бы у меня были следующие три определения нового типа: 

newtype PayloadA = PA Int
newtype PayloadB = PB Double
newtype PayloadC = PC Bool

Есть ли способ убедить GH C дать мне это?

Ответы [ 2 ]

7 голосов
/ 16 февраля 2020

Это выглядит невозможным, по крайней мере, с текущим GH C. Предположим, что у вашего Payload A было то же представление Int и т. Д. 

data Tag = A | B | C

data Payload (tag :: Tag) where
  PA :: Int -> Payload A
  PB :: Double -> Payload B
  PC :: Bool -> Payload C

Тогда как нам это реализовать? 

foo :: Payload tag -> Int
foo (PA i) = i
foo (PB _) = 1
foo (PC _) = 2

Для реализации foo, нам как-то нужно извлечь tag из Payload tag, но это невозможно, если Payload tag не хранит тег в его представлении.

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

type family Payload (tag :: Tag) where
   Payload 'A = Int
   Payload 'B = Double
   Payload 'C = Bool

Теперь Payload 'A - это точно Int. Однако мы теряем возможность писать foo, поскольку тег больше не сохраняется во время выполнения вдоль полезной нагрузки. Вместо этого мы можем написать это: 

-- singleton, could be auto-generated using the singletons library
data STag (tag :: Tag) where
    SA :: STag 'A
    SB :: STag 'B
    SC :: STag 'C

bar :: STag tag -> Payload tag -> Int
bar PA i = i
bar PB _ = 1
bar PC _ = 2

Обратите внимание, как мы по существу добавляем тег в качестве аргумента, поскольку нам нужно, чтобы он был представлен во время выполнения.

5 голосов
/ 16 февраля 2020

Вы можете сделать так: 

data family Payload (tag :: Tag)
newtype instance Payload A = PA Int
newtype instance Payload B = PB Double
newtype instance Payload C = PC Bool

Это соответствует вашему требованию иметь типы, отличные от Int, Double, Bool, и иметь семантику операций нового типа. Конечно, цена, которую вы платите, заключается в том, что вы не сможете сопоставить образец, чтобы определить, что есть что. Но вы можете восстановить такие вещи с помощью класса типов или явно передавая тег (который в большинстве случаев означает то же самое под капотом); например: 

class Foo (t :: Tag) where foo :: Payload t -> Int
instance Foo A where foo (PA i) = i
instance Foo B where foo (PB _) = 2
instance Foo C where foo (PC _) = 3
...