Доступ к ограничениям GET с уровня оценки

Question

Доступ к ограничениям GET с уровня оценки

Другая возможная причина: убедитесь, что вы случайно не дали обоим проектам одно и то же имя сборки в свойствах проекта.

2

dependent-type gadt haskell

задан radrow 17 January 2019 в 13:10

1 ответ

Другие вопросы по тегам:

dependent-type gadt haskell

Похожие вопросы:

score 0 · Answer 1

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

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

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

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

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