Тип уровня Haskell буквальный Nat: статус?

Question

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

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

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

Комментарий 18 из this page упоминает этот простой пример размера параметризованных ЗВТ (я добавил ЯЗЫКА прагмами и оператор импорта):

{-# 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) 

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

Answer 1

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

Человек, которого я знаю, который наиболее активно занимается этой проблемой, является одним Iavor Diatchki. Эта бумага стоит за немой платой ACM, но вы можете найти его Haskell Symposium 2015 talk here on YouTube - это очень хорошо объяснено !. Его разговор использует тот же пример, что и ваш, всегда популярный вектор. His branch in the GHC repository работает над тем, чтобы слить его в магистральный GHC, но насколько я знаю, даты не установлены. Пока вы должны использовать плагин typechecker, что не так уж плохо. В конце концов, оригинал goal of Plugins/Typechecker должен был включить интересную работу, подобную этой, без необходимости объединять все в исходный код. Есть кое-что, что можно сказать о модульности!