Instantiiertyp Variable in Haskell

Question

BEARBEITEN: Gelöst. Ich wusste nicht, dass das Aktivieren einer Spracherweiterung in der Quelldatei die Spracherweiterung in GHCi nicht aktiviert hat. Die Lösung war :set FlexibleContexts in GHCi.

Ich habe kürzlich entdeckt, dass Typdeklarationen in Klassen und Instanzen in Haskell Horn-Klauseln sind. Also habe ich die arithmetischen Operationen von The Art of Prolog, Kapitel 3 in Haskell codiert. Zum Beispiel:

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 werden Werte für (logische) Variable in einem Beweis instanziiert. Ich verstehe jedoch nicht, wie man Typvariablen in Haskell instanziiert. Das heißt, ich verstehe nicht, was das Haskell-Äquivalent einer Prolog-Abfrage

ist. Ich gehe davon aus, dass

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

verursachen würde Haskell xi instanziiert, aber das gibt einen Non type-variable argument in the constraint Fehler, auch mit FlexibleContexts aktiviert.

Answer 1

Nein sicher Prolog Proben, aber ich würde in der folgenden Art und Weise dies in Haskell definieren:

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

Update:

Wie danportin notierte in seinem Kommentar unter TypeFamilies "Faule Muster" (im Beispielkontext) wird hier nicht benötigt (sein Anfangscode ist kürzer und viel sauberer). obwohl

Eine Anwendung dieses Muster, das ich von im Zusammenhang mit dieser Frage denken kann, ist dies: Sagen wir Boolesche Logik auf unsere Art-Level-Arithmetik hinzufügen möchten:

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 

aber dies wird nicht Kompilieren wegen "Konflikt der funktionalen Abhängigkeiten". Und es scheint mir, dass wir immer noch diese überlappend Fall ohne fundeps ausdrücken können:

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 

Es ist definitiv kein schönste Art und Weise (es erfordert IncoherentInstances). Vielleicht kann jemand einen anderen, weniger traumatischen Ansatz vorschlagen.