Instantiate type variable in Haskell

Question

EDIT: Solved. I was unware that enabling a language extension in the source file did not enable the language extension in GHCi. The solution was to :set FlexibleContexts in GHCi.

---

I recently discovered that type declarations in classes and instances in Haskell are Horn clauses. So I encoded the arithmetic operations from The Art of Prolog, Chapter 3, into Haskell. For instance:

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, values are instantiated for (logic) variable in a proof. However, I don't understand how to instantiate type variables in Haskell. That is, I don't understand what the Haskell equivalent of a Prolog query

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

is. I assume that

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

would cause Haskell to instantiate xi, but this gives a Non type-variable argument in the constraint error, even with FlexibleContexts enabled.

Answer 1

No sure about Prolog samples, but I would define this in Haskell in the following way:

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

As danportin noted in his comment below TypeFamilies "Lazy pattern" (in instance context) is not needed here (his initial code is shorter and much cleaner).

One application of this pattern though, which I can think of in the context of this question is this: Say we want to add Boolean logic to our type-level arithmetic:

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

But this will not compile due to "Functional dependencies conflict". And it looks to me that we still can express this overlapping case without 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

It's definitely not a nicest way (it requires IncoherentInstances). So maybe somebody can suggest another, less 'traumatic' approach.