Parametrizzazione dei tipi per interi in Haskell

Question

Sto cercando di creare alcuni tipi di Haskell parametrizzati non dai tipi ma dagli elementi di un tipo, in particolare, gli interi. Ad esempio, un vettore (lineare-algebra) in R^2 e un vettore in R^3 sono diversi oggetti tipizzati. Nello specifico, sto scrivendo un albero K-D in Haskell e voglio parametrizzare la mia struttura dati con un numero intero positivo, quindi un albero 3D e un albero 4-D hanno un tipo diverso.

Ho provato a parametrizzare il mio albero con le tuple, ma non sembra andare da nessuna parte (e sembra alquanto improbabile che questo possa essere spinto attraverso, soprattutto perché non sembra che le triple o le più grandi siano anche funtori (e non so alcun modo per dire come, esempio HomogeneousTuple a => Functor a) voglio fare qualcosa del genere:.

data (TupleOfDoubles a) => KDTree a b = ... ---so in a 3DTree a is (Double,Double,Double) 

che sarebbe bello, o qualcosa di simile sarebbe altrettanto buono

data KDTree Int a = ... -- The Int is k, so KDTree has kind Int -> * -> * 

Qualcuno sa se uno di questi gli effetti sono praticabili o ragionevoli?

Grazie -Joseph

Answer 1

C'è un GHC estensione in lavorazione chiamato TypeNats, che sarebbe esattamente quello che vuoi. Tuttavia il traguardo per questo è attualmente impostato su 7.4.1 in base allo the ticket, quindi sarà ancora un po 'di attesa.

Fino a quando quell'estensione è disponibile, l'unica cosa che puoi fare è codificare la dimensione usando i tipi. Per esempio qualcosa in questo senso potrebbe funzionare:

{-# LANGUAGE ScopedTypeVariables #-} 
class MyTypeNat a where 
    toInteger :: a -> Integer 

data Zero 
data Succ a 

instance MyTypeNat Zero where 
    toInteger _ = 0 

instance MyTypeNat a => MyTypeNat (Succ a) where 
    toInteger _ = toInteger (undefined :: a) + 1 

data KDTree a b = -- ... 

dimension :: forall a b. MyTypeNat a => KDTree a b -> Integer 
dimension = toInteger (undefined :: a) 

Il rovescio della medaglia di un approccio come questo è, naturalmente, che si deve scrivere qualcosa di simile KDTree (Succ (Succ (Succ Zero))) Foo invece di KDTree 3 Foo.

Answer 2

La risposta di sepp2k mostra l'approccio di base per farlo. In effetti, gran parte del lavoro è già stato fatto.

Type livello pacchetti numero

• natural-number e type-level-natural-number
• numtype
• type-level

Stuff usando livello tipo codifiche di numeri naturali (esempi)

• Vec
• Dimensional
• llvm
• ForSyDe

Purtroppo qualcosa di simile:

data KDTree Int a = ... 

non è davvero possibile. Il tipo finale (creato da KDTree) dipende dal valore di Int, che richiede una funzione denominata tipi dipendenti.Lingue come Agda ed Epigram supportano questo, ma non Haskell.