Istanze basate su predicato a livello di livello?

Question

creare una classe tipo che accetta il tipo di prodotti naturali a livello Z, (SZ), (S (SZ)) ... ecc, si può semplicemente dichiarare le istanze in modo ricorsivo in quanto tale:

data Z 
data S a 

class Type a 

instance Type Z 
instance Type (S a) 

E ' possibile creare un'istanza di classe tipo basata su predicati a livello di tipo? Per esempio, io voglio essere in grado di dire:

{-# LANGUAGE MultiParamTypeClasses #-} 
class Type a b 
instance Type x y when (x :+: y == 8) 

Dove :+: è digitare aggiunta di livello, e == è di tipo a livello di uguaglianza da Data.Type.Equality, in modo che le istanze vengono create solo per coppie di NAT che aggiungono fino a 8

La notazione è simile a questa disponibile in Haskell? Altrimenti, come si compirebbe qualcosa del genere?

Edit: Questo post è stato ispirato by the Haskell wiki article on smart constructors, dove una classe di tipo InBounds è stato dichiarato per verificare staticamente che l'argomento di tipo phantom passato a un costruttore intelligente fosse in qualche gamma di Nat s, il costruttore intelligente era:

resistor :: InBounds size => size -> Resistor size 
resistor _ = Resistor 

Cercando di fare qualcosa di simile nel mio esempio (dopo aver usato la risposta di leftaroundabout) mi dà un errore:

construct :: (Type a b) => a -> b -> MyType a b 
construct _ _ = MyType 

>>> Expected a type, but a has kind Nat… 

l'esempio dal wiki Haskell funziona perché doesn' t utilizzare DataKinds, è possibile passare un tipo di tipo Nat a una funzione a livello di valore?

Answer 1

È necessario utilizzare non un predicato di uguaglianza ma un vincolo di uguaglianza (che viene inserito nella lingua, abilitare con -XGADTs).

{-# LANGUAGE KindSignatures, DataKinds, MultiParamTypeClasses, FlexibleInstances, GADTs #-} 

import GHC.TypeLits 

class Type (a :: Nat) (b :: Nat) 

instance (a + b) ~ 8 => Type a b 

mente che questo non è necessariamente così utile come potrebbe sembrare - il vincolo di uguaglianza non lo fa in qualche modo enumerare tutte le combinazioni che aggiungono fino a 8, invece consente a tutti Nat -pairs di essere esempio , richiede solo una prova pari a che aggiungono fino a 8. Questa prova è possibile utilizzare, ma dubito che Haskell sia ancora solo ordinamento di -dipendentemente dalla natura tipizzata rende questo lavoro davvero ottimo.

Answer 2

si potrebbe scrivere una funzione di livello di tipo

type family NatEq (a :: Nat) (b :: Nat) :: Bool 
type instance NatEq 0 0 = True 
... 

E poi

instance Type' (NatEq (a + b) 8) a b => Type a b 
class Type' (x :: Bool) (a :: Nat) (b :: Nat) where ... 
instance Type' True a b where ... 
-- If you wanted a different behaviour otherwise: 
-- instance Type' False a b where ... 

È necessario attivare un gruppo di estensioni, naturalmente.

Questo funziona correttamente se a e b sono costanti, in modo che a+b può essere ridotto a 8 (o un'altra costante). Se non sono costanti, non aspettarti che GHC provi l'equazione per te. Cioè (usando Int invece di Nat), non aspettatevi che Type x (8-x) sia risolto.