Listy o stałej długości i typie literowym

Question

Próbuję zdefiniować typ dla list o stałej długości w Haskell. Kiedy używam standardowego sposobu kodowania liczb naturalnych jako typów w trybie jednoargumentowym, wszystko działa poprawnie. Jednak kiedy próbuję budować wszystko na literałach typu GHC, napotykam mnóstwo problemów.

Mój pierwszy strzał w żądanym typu listy był

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

które niestety nie pozwalają na pisanie funkcji zip z rodzaju

zip :: List n a -> List n b -> List n (a,b) 

mogę rozwiązać ten problem poprzez odjęcie 1 od typ zmienna n w typie (:>):

data List (n :: Nat) a where 
    Nil :: List 0 a 
    (:>) :: a -> List (n-1) a -> List n a -- subtracted 1 from both n's 

Następnie próbowałem zdefiniować funkcję append:

append :: List n1 a -> List n2 a -> List (n1 + n2) a 
append Nil  ys = ys 
append (x :> xs) ys = x :> (append xs ys) 

Niestety, GHC mówi mi

Couldn't match type ‘(n1 + n2) - 1’ with ‘(n1 - 1) + n2’ 

Dodanie ograniczenia ((n1 + n2) - 1) ~ ((n1 - 1) + n2) do podpisu nie rozwiązuje problemów, ponieważ GHC narzeka

Could not deduce ((((n1 - 1) - 1) + n2) ~ (((n1 + n2) - 1) - 1)) 
from the context (((n1 + n2) - 1) ~ ((n1 - 1) + n2)) 

Teraz, oczywiście, złapałem jakąś nieskończoną pętlę.

Chciałbym więc wiedzieć, czy możliwe jest zdefiniowanie typu dla list o stałej długości przy użyciu literałów typu w ogóle. Czy mógłbym nawet nadzorować bibliotekę właśnie w tym celu? Zasadniczo jedynym wymaganiem jest to, że chcę napisać coś w stylu List 3 a zamiast .

Answer 1

To nie jest odpowiedź.

Korzystanie https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2 ten

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} 

import GHC.TypeLits 

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

append :: List n1 a -> List n2 a -> List (n1 + n2) a 
append Nil  ys = ys 
append (x :> xs) ys = x :> (append xs ys) 

... kompiluje, więc oczywiście jest to poprawne.

Answer 2

Literały z liczbą poziomów typu nie mają jeszcze struktury, na której możemy wykonać indukcję, a wbudowany program do rozwiązywania ograniczeń może wykryć tylko najprostsze przypadki. Obecnie lepiej trzymać się Peano naturals.

Jednak nadal możemy używać literałów jako cukru syntaktycznego.

{-# LANGUAGE 
    UndecidableInstances, 
    DataKinds, TypeOperators, TypeFamilies #-} 

import qualified GHC.TypeLits as Lit 

data Nat = Z | S Nat 

type family Lit n where 
    Lit 0 = Z 
    Lit n = S (Lit (n Lit.- 1)) 

Teraz można napisać List (Lit 3) a zamiast .