Instantiate type variable in Haskell
- by danportin
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 insantiated 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.
