Я пытаюсь понять GHC.TypeLits и конкретно someNatVal. Я понимаю, как это используется в этом блоге опубликовать здесь, но, как уже упоминалось, тот же пример можно было бы реализовать с использованием natVal, например:
isLength :: forall len a. KnownNat len => Integer -> List len a -> Bool
isLength n _ = n == natVal (Proxy :: Proxy len)
Есть ли варианты использования someNatVal, которые нельзя переписать с помощью natVal?
SomeNat экзистенциально квантифицируется:
data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
который читается как SomeNat, содержит, ну, "некоторые n :: Nat". Proxy — это синглтон, который позволяет поднять n на уровень типов, чтобы удовлетворить систему типов — в языке с зависимой типизацией такая конструкция нужна очень редко. Мы можем определить SomeNat более явно, используя GADTs:
data SomeNat where
SomeNat :: forall n. KnownNat n => Proxy n -> SomeNat
Таким образом, SomeNat содержит Nat, который неизвестен статически.
потом
someNatVal :: Integer -> Maybe SomeNat
читается как «someNatVal получает Integer, а Maybe возвращает скрытое Nat». Мы не можем вернуть KnownNat, потому что Known означает "известно на уровне типа", но мы ничего не знаем о произвольном Integer на уровне типа.
Обратное (по модулю SomeNat оболочка и proxy вместо Proxy) someNatVal равно
natVal :: forall n proxy. KnownNat n => proxy n -> Integer
Читается как «natVal получает что-то, что имеет Nat в своем типе, и возвращает это Nat, преобразованное в Integer».
Экзистенциально-количественные типы данных обычно используются для переноса значений времени выполнения. Скажем, вы хотите прочитать Vec (список со статически известной длиной) из STDIN, но как бы вы статически вычислили длину ввода? Выхода нет. Таким образом, вы оборачиваете список, который вы прочитали, в соответствующий экзистенциально квантифицированный тип данных, тем самым говоря: «Я не знаю длины, но она существует».
Однако во многих случаях это излишне. Чтобы сделать что-то с экзистенциально количественным типом данных, вам нужно быть общим: например. если вам нужно найти сумму элементов SomeVec, вы должны определить sumVec для Vec с произвольной длиной. Затем вы разворачиваете SomeVec и применяете sumVec, тем самым говоря: «Я не знаю длину обернутого Vec, но sumVec все равно». Но вместо этой упаковки-развертки вы можете напрямую использовать CPS.
Однако из-за этой общности вам необходимо включить ImpredicativeTypes, чтобы иметь возможность определять, скажем, список с такими продолжениями. В этом случае список с экзистенциально количественными данными представляет собой общий шаблон, который позволяет обойти ImpredicativeTypes.
Что касается вашего примера, с правильно определенными Nats версия, которая сравнивает Nats, ленивее, чем версия, которая сравнивает Integers.
Основное использование someNatVal — это использование значения во время выполнения, как если бы это был тип, который не был известен во время компиляции.
Мой ответ на Могу ли я получить неизвестный KnownNat? предоставляет действительно тупой пример. Есть миллион лучших способов написать программу, которая делает то же самое, что и эта. Но это показывает, что делает someNatVal. По сути, это функция от значения к типу — с экзистенциальным ограничением области действия этого типа местами, где он статически неизвестен.
let b = Bar "foo" :: Bar n in show b?
- person jberryman; 09.09.2015
n. Как тип n точно соответствует значению, указанному во время выполнения? В конце концов, типы существуют только во время компиляции в Haskell. Это то, что делает someNatVal.
- person Carl; 09.09.2015
