Уровень типа Haskell literal Nat: статус?

GHC имеет тип литературного уровня Nats. Я могу кое-что прочитать о них, например, здесь:

https://ghc.haskell.org/trac/ghc/wiki/TypeNats

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

Комментарий 18 из этой страницы упоминает этот простой пример параметризованных параметров Vecs (я добавил прагмы LANGUAGE и оператор импорта):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits

data Vec :: Nat -> * -> * where
  Nil  :: Vec 0 a
  (:>) :: a -> Vec n a -> Vec (n+1) a

(+++) :: Vec n a -> Vec m a -> Vec (n+m) a
Nil       +++ bs = bs
(a :> as) +++ bs = a :> (as +++ bs)

В то время это не работало, но затем реализация была модифицирована так, чтобы это сработало. Это было 5 лет назад... но это не работает на моем GHC 7.10.1:

trash.hs:15:20:
    Could not deduce ((n + m) ~ ((n1 + m) + 1))
    from the context (n ~ (n1 + 1))
      bound by a pattern with constructor
                 :> :: forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a,
               in an equation for ‘+++’
      at trash.hs:15:2-8
    NB: ‘+’ is a type function, and may not be injective
    Expected type: Vec (n + m) a
      Actual type: Vec ((n1 + m) + 1) a
    Relevant bindings include
      bs :: Vec m a (bound at trash.hs:15:15)
      as :: Vec n1 a (bound at trash.hs:15:7)
      (+++) :: Vec n a -> Vec m a -> Vec (n + m) a
        (bound at trash.hs:14:1)
    In the expression: a :> (as +++ bs)
    In an equation for ‘+++’: (a :> as) +++ bs = a :> (as +++ bs)

Какая сделка здесь? Являются ли тип литературного уровня Натсом приемлемым для такого рода вещей? Если да, то каким образом я могу реализовать функцию (+++)? Если нет, то в чем их прецедент?

Ответы

Ответ 1

Как уже отмечали комментаторы, typechecker в настоящее время не может выполнить это равенство, потому что для этого требуется алгебра. Принимая во внимание, что вы и я знаем, что n + m = n1 + m + 1 задано n = n1 + 1, никто не учил методу GHC typechecker, как выполнять такую ​​арифметику. На таких языках, как Ada, Idris или Coq, вы могли бы обучить компилятор этим правилам или, возможно, правила арифметики были бы предоставлены вам в библиотеке, но в Haskell тип typechecker немного более жесткий (но гораздо более дружелюбный к реальному программированию, на мой взгляд), и вам, к сожалению, прибегнуть к плагину typechecker.

Человек, которого я знаю, который наиболее активно занимается этой проблемой, - это "Яворный Diatchki" . Этот документ стоит за немым плагином ACM, но вы можете найти его Haskell Symposium 2015 здесь, на YouTube - это очень хорошо объяснено!. Его разговор использует тот же пример, что и ваш, всегда популярный вектор. Его филиал в репозитории GHC работает над объединением его в магистральный GHC, но насколько я знаю, даты не установлены. Пока вы должны использовать плагин typechecker, что не так уж плохо. В конце концов, оригинальная цель Plugins/Typechecker заключалась в том, чтобы включить интересную работу, подобную этой, без необходимости объединять все в исходный код. Там что-то нужно сказать для модульности!