Variable de tipo de instancia en Haskell

Question

EDIT: Solucionado. No estaba al tanto de que habilitar una extensión de idioma en el archivo fuente no permitía la extensión de idioma en GHCi. La solución fue :set FlexibleContexts en GHCi.

---

Recientemente descubrí que las declaraciones de tipo en clases e instancias en Haskell son cláusulas Horn. Así que codifiqué las operaciones aritméticas de The Art of Prolog, Capítulo 3, en Haskell. Por ejemplo:

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 

En Prolog, los valores se instancian para la variable (lógica) en una prueba. Sin embargo, no entiendo cómo crear instancias de variables de tipo en Haskell. Es decir, no entiendo cuál es el equivalente de Haskell de una consulta de Prolog

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

es. Asumo que

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

causaría Haskell crear una instancia de xi, pero esto da un error Non type-variable argument in the constraint, incluso con FlexibleContexts habilitado.

Answer 1

no está seguro acerca de las muestras de Prolog, pero yo definiría esta en Haskell de la siguiente manera:

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

Actualización:

Como danportin señaló en su comentario a continuación TypeFamilies "patrón perezoso" (en el contexto de la instancia) no es necesario aquí (su código inicial es más corto y mucho más limpio).

Una aplicación de este modelo, sin embargo, lo que se me ocurre en el contexto de esta pregunta es la siguiente: Digamos que queremos añadir la lógica booleana para nuestra aritmética de nivel tipo:

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 

pero esto no será compilar debido a "conflicto de dependencias funcionales". y parece a mí que todavía podemos expresar este caso, sin superposición 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 

Definitivamente no es una forma más amable (que requiere IncoherentInstances). Entonces, tal vez alguien pueda sugerir otro enfoque menos "traumático".