Listen von Literalen fester Länge und Typ

Question

Ich versuche, einen Typ für Listen fester Länge in Haskell zu definieren. Wenn ich den Standardweg nutze, um natürliche Zahlen als unäre Typen zu kodieren, funktioniert alles gut. Wenn ich jedoch versuche, alles auf GHC-Typ-Literalen aufzubauen, stoße ich auf viele Probleme.

Mein erster Schuss auf den Typ gewünschte Liste war

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

die leider nicht zum Schreiben einer Zip-Funktion mit Typ

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

zuließ ich durch Subtrahieren von 1 von der Lösung dieses Problems könnte Typ Variable n in der Art von (:>):

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

Als nächstes habe ich versucht, eine Append-Funktion zu definieren:

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

Leider GHC sagt mir

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

Hinzufügen der Einschränkung ((n1 + n2) - 1) ~ ((n1 - 1) + n2) zur Unterzeichnung löst nicht die Probleme, da GHC

klagt

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

Jetzt bin ich offensichtlich in einer Art Endlosschleife gefangen.

Also ich würde gerne wissen, ob es möglich ist, einen Typ für Listen fester Länge mit Hilfe von Typ Literalen überhaupt zu definieren. Habe ich vielleicht sogar genau zu diesem Zweck eine Bibliothek beaufsichtigt? Im Grunde ist die einzige Voraussetzung, dass ich etwas wie List 3 a anstelle von schreiben möchte.

Answer 1

Dies ist nicht wirklich eine Antwort.

https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2 Mit dieser

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

... kompiliert, so offensichtlich richtig es ist.

Answer 2

Typ-Level-Nummern-Literale haben noch keine Struktur, auf der wir Induktion durchführen können, und der eingebaute Constraint-Solver kann nur die einfachsten Fälle herausfinden. Momentan ist es besser, mit Peano Naturals zu bleiben.

Allerdings können wir die Literale immer noch als syntaktischen Zucker verwenden.

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

Jetzt können Sie List (Lit 3) a statt schreiben.