Получите доступ к GADT с уровня оценки - PullRequest
Новая
       41

Получите доступ к GADT с уровня оценки

0 голосов
/ 17 января 2019

Я пытаюсь использовать некоторые параметры GADT из среды выполнения, предполагая, что я использовал расширение DataKinds, чтобы разрешить преобразование данных в типы. то есть имея 

data Num = Zero | Succ Num
data Something (len :: Num) where
  Some :: Something len

Я бы хотел иметь функцию 

toNum :: Something len -> Num

, что для любого Some :: Something n вернет n: 

toNum (s :: Something n) = n

Что недопустимо в Хаскеле. Возможно ли это сделать?

1 Ответ

0 голосов
/ 17 января 2019

В Haskell это невозможно, так как типы стираются во время выполнения. То есть, когда программа запустится, в памяти нет информации о значении индекса let в типе.

Чтобы преодолеть эту проблему, нам нужно заставить Haskell сохранять в памяти это значение во время выполнения. Обычно это делается с использованием вспомогательного типа singleton : 

data Num = Zero | Succ Num

data SNum (n :: Num) where
   SZero :: SNum 'Zero
   SSucc :: SNum n -> SNum ('Succ n)

data Something (len :: Num) where
  Some :: SNum len -> Something len

Используя это, вы можете легко написать 

sToNum :: SNum n -> Num
sToNum SZero = Zero
sToNum (SSucc n) = Succ (sToNum n)

, а затем 

toNum :: Something len -> Num
toNum (Some n) = sToNum n

Если вы ищите "haskell singletons", вы должны найти несколько примеров. Есть даже библиотека singletons, чтобы частично автоматизировать это.

Если / когда будет выпущен «зависимый Haskell», у нас будут менее громоздкие инструменты. В настоящее время синглтоны работают, но иногда они доставляют хлопоты. Тем не менее, на данный момент мы должны использовать их.

...