tipo di variabile Instantiate in Haskell

Question

EDIT:. Risolto ero ignaro che permette un'estensione del linguaggio nel file di origine non ha consentito l'estensione lingua in GHCi. La soluzione era quella di :set FlexibleContexts in GHCi.

---

Di recente ho scoperto che le dichiarazioni di tipo nelle classi e le istanze a Haskell sono clausole di Horn. Così ho codificato le operazioni aritmetiche da The Art of Prolog , capitolo 3, in Haskell. Per esempio:

fac(0,s(0)).
fac(s(N),F) :- fac(N,X), mult(s(N),X,F).

class Fac x y | x -> y
instance Fac Z (S Z)
instance (Fac n x, Mult (S n) x f) => Fac (S n) f

pow(s(X),0,0) :- nat(X).
pow(0,s(X),s(0)) :- nat(X).
pow(s(N),X,Y) :- pow(N,X,Z), mult(Z,X,Y).

class Pow x y z | x y -> z
instance (N n) => Pow (S n) Z Z
instance (N n) => Pow Z (S n) (S Z)
instance (Pow n x z, Mult z x y) => Pow (S n) x y

In Prolog, valori vengono istanziata per la variabile (logica) in una prova. Tuttavia, non capisco come creare un'istanza variabili di tipo in Haskell. Cioè, non capisco quale sia l'equivalente di un Haskell Prolog interrogazione

?-f(X1,X2,...,Xn)

è. Suppongo che

:t undefined :: (f x1 x2 ... xn) => xi

causerebbe Haskell a xi instantiate, ma questo dà un errore di Non type-variable argument in the constraint, anche con FlexibleContexts abilitato.

Answer 1

Non sono sicuro campioni Prolog, ma vorrei definire questo in Haskell nel seguente modo:

{-# LANGUAGE MultiParamTypeClasses, EmptyDataDecls, FlexibleInstances,
FlexibleContexts, UndecidableInstances, TypeFamilies, ScopedTypeVariables #-}

data Z
data S a
type One = S Z
type Two = S One
type Three = S Two
type Four = S Three 


class Plus x y r
instance (r ~ a) => Plus Z a r
instance (Plus a b p, r ~ S p) => Plus (S a) b r

p1 = undefined :: (Plus Two Three r) => r


class Mult x y r
instance (r ~ Z) => Mult Z a r
instance (Mult a b m, Plus m b r) => Mult (S a) b r

m1 = undefined :: (Mult Two Four r) => r


class Fac x r
instance (r ~ One) => Fac Z r
instance (Fac n r1, Mult (S n) r1 r) => Fac (S n) r

f1 = undefined :: (Fac Three r) => r


class Pow x y r
instance (r ~ One) => Pow x Z r
instance (r ~ Z) => Pow Z y r
instance (Pow x y z, Mult z x r) => Pow x (S y) r

pw1 = undefined :: (Pow Two Four r) => r

-- Handy output
class (Num n) => ToNum a n where
    toNum :: a -> n
instance (Num n) => ToNum Z n where
    toNum _ = 0
instance (ToNum a n) => ToNum (S a) n where
    toNum _ = 1 + toNum (undefined :: a) 

main = print $ (toNum p1, toNum m1, toNum f1, toNum pw1)

Aggiornamento:

Come danportin annotò nel suo commento qui sotto TypeFamilies "Lazy pattern" (in un contesto esempio) non è necessario qui (il suo codice iniziale è più breve e molto più pulito).

Un'applicazione di questo modello, però, che mi viene in mente nel contesto di questa domanda è questa: diciamo che vogliamo aggiungere la logica booleana per la nostra aritmetica tipo di livello:

data HTrue
data HFalse

-- Will not compile
class And x y r | x y -> r
instance And HTrue HTrue HTrue
instance And a b HFalse -- we do not what to enumerate all the combination here - they all HFalse

Ma questo non verrà compilato a causa di "Dipendenze funzionali conflitto". E mi sembra che siamo ancora in grado di esprimere questo caso si sovrappongono senza fundeps:

class And x y r
instance (r ~ HTrue) => And HTrue HTrue r
instance (r ~ HFalse) => And a b r

b1 = undefined :: And HTrue HTrue r => r   -- HTrue
b2 = undefined :: And HTrue HFalse r => r  -- HFalse

Non è sicuramente un modo più bello (richiede IncoherentInstances). Quindi forse qualcuno può suggerire un altro, meno approccio 'traumatico'.