Zmienna typu instancji w Haskell

Question

EDYCJA: Rozwiązany. Nie wiedziałem, że włączenie rozszerzenia językowego w pliku źródłowym nie umożliwiło rozszerzenia języka w GHCi. Rozwiązaniem było :set FlexibleContexts w GHCi.

---

Niedawno odkryłem, że deklaracje typów w klasach i instancjach w Haskell są klauzulami Horn. Więc zakodowałem operacje arytmetyczne z Art of Prolog, rozdział 3, na Haskella. Na przykład:

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 

W Prologu wartości są tworzone dla zmiennej (logicznej) w dowodzie. Jednak nie rozumiem, jak utworzyć instancję zmiennych typu Haskell. To znaczy, nie rozumiem, jaki jest odpowiednik Haskella w zapytaniu Prologa. Zakładam, że

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

spowodowałoby Haskell instancji xi, ale daje to błąd Non type-variable argument in the constraint, nawet z FlexibleContexts włączone.

Answer 1

Nie pewny próbek Prolog, ale ja bym zdefiniował tego w Haskell w następujący sposób:

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

Aktualizacja:

Jak danportin zanotował w swoim komentarzu poniżej TypeFamilies "Lazy wzorca" (w kontekście instancji) nie jest tu potrzebny (jego początkowy kod jest krótszy i znacznie czystszy).

Jednym z zastosowań tego wzoru choć, co mogę myśleć w kontekście tego pytania to: Powiedzmy, że chcemy dodać logiczną logiki do naszej typ poziomie arytmetyki:

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 

Ale to nie będzie kompilacja z powodu "Konfliktów zależności funkcjonalnych". I wygląda mi się, że nadal możemy wyrazić to nakładającą sprawy bez 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 

To nie jest zdecydowanie najpiękniejszy sposób (wymaga IncoherentInstances). Być może ktoś może zaproponować inne, mniej "traumatyczne" podejście.