Elenchi di lunghezza fissa e letterali tipo

Question

Sto provando a definire un tipo per gli elenchi di lunghezza fissa in Haskell. Quando uso il modo standard per codificare i numeri naturali come tipi in unario, tutto funziona correttamente. Tuttavia, quando cerco di costruire tutto su letterali di tipo GHC, mi imbatto in tonnellate di problemi.

Il mio primo colpo al tipo di elenco desiderato era

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

che purtroppo non ha permesso per la scrittura di una funzione di cerniera con il tipo

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

ho potuto risolvere questo problema sottraendo 1 dal digitare la variabile n nel tipo di (:>):

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

Successivamente, ho cercato di definire una funzione di accodamento:

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

Purtroppo, GHC mi dice

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

Aggiunta del vincolo ((n1 + n2) - 1) ~ ((n1 - 1) + n2) alla firma non risolve i problemi poiché GHC lamenta

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

Ora, sono ovviamente preso in una specie di loop infinito.

Quindi, mi piacerebbe sapere se è possibile definire un tipo per gli elenchi di lunghezza fissa utilizzando letterali di tipo affatto. Forse ho anche supervisionato una biblioteca proprio per questo scopo? Fondamentalmente, l'unico requisito è che voglio scrivere qualcosa come List 3 a anziché .

Answer 1

Questa non è davvero una risposta.

Utilizzando https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2, questo

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

... compila, quindi ovviamente è corretto.

Answer 2

I letterali dei numeri di livello dei tipi non hanno ancora una struttura su cui possiamo eseguire l'induzione e il risolutore di vincoli incorporato può solo individuare i casi più semplici. Attualmente è meglio attenersi ai prodotti naturali di Peano.

Tuttavia, possiamo ancora usare i letterali come zucchero sintattico.

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

Ora è possibile scrivere List (Lit 3) a invece di .