El sistema de tipos y la programación lógica de Haskell: cómo portar programas de Prolog a nivel de tipo

type-systems logic-programming

Question

Estoy tratando de entender la relación entre un lenguaje de programación lógico (Prolog en mi caso) y el sistema de tipos de Haskell.

Sé que ambos usan la unificación y las variables para encontrar valores (o tipos, en el sistema de tipos de Haskell) dependiendo de las relaciones. Como ejercicio para comprender mejor las similitudes y diferencias entre ellos, traté de reescribir algunos programas de prólogo simples en el nivel de tipo de Haskell, pero tengo problemas con algunas partes.

Primero, reescribí este sencillo programa de prólogo:

numeral(0).
numeral(succ(X)) :- numeral(X).

add(0,Y,Y).
add(succ(X),Y,succ(Z)) :- add(X,Y,Z).

como:

class Numeral a where
    numeral :: a
    numeral = u

data Zero
data Succ a

instance Numeral Zero
instance (Numeral a) => Numeral (Succ a)

class (Numeral a, Numeral b, Numeral c) => Add a b c | b c -> a where
    add :: b -> c -> a
    add = u

instance (Numeral a) => Add a Zero a
instance (Add x y z) => Add (Succ x) (Succ y) z

funciona bien, pero no pude extenderlo con este Prolog:

greater_than(succ(_),0).
greater_than(succ(X),succ(Y)) :- greater_than(X,Y).

Lo que intenté fue esto:

class Boolean a
data BTrue
data BFalse
instance Boolean BTrue
instance Boolean BFalse

class (Numeral a, Numeral b, Boolean r) => Greaterthan a b r | a b -> r where
    greaterthan :: a -> b -> r
    greaterthan = u

instance Greaterthan Zero Zero BFalse
instance (Numeral a) => Greaterthan (Succ a) Zero BTrue
instance (Numeral a) => Greaterthan Zero (Succ a) BFalse
instance (Greaterthan a b BTrue)  => Greaterthan (Succ a) (Succ b) BTrue
instance (Greaterthan a b BFalse) => Greaterthan (Succ a) (Succ b) BFalse

El problema con este código es que las dos últimas instancias están causando un conflicto fundep. Puedo entender por qué, pero me parece que no debería ser un problema ya que sus partes de guardia (o como se llame, me refiero a la (Greaterthan abc) => ) son diferentes, por lo que a s y b s en las últimas dos declaraciones de cumplimiento son en realidad valores diferentes y no hay conflictos.

Otro programa que intenté reescribir fue este:

child(anne,bridget).
child(bridget,caroline).
child(caroline,donna).
child(donna,emily).

descend(X,Y) :- child(X,Y).
descend(X,Y) :- child(X,Z),
                descend(Z,Y).

(por cierto, los ejemplos son del libro Learn Prolog Now )

data Anne
data Bridget
data Caroline
data Donna
data Emily

class Child a b | a -> b where
    child :: a -> b
    child = u

instance Child Anne Bridget
instance Child Bridget Caroline
instance Child Caroline Donna
instance Child Donna Emily

class Descend a b | b -> a where
    descend :: b -> a
    descend = u

instance (Child a b) => Descend a b
instance (Child a c, Descend c b) => Descend a b

Y me aparece el error "duplicar instancias" en la última línea. Creo que es un problema similar, incluso si tengo partes de guardia diferentes, recibo errores porque las partes del cuerpo (me refiero a las partes Descend ab ) son las mismas.

Así que estoy buscando formas de trasladar los programas Prolog al nivel de tipo de Haskell, si es posible. Cualquier ayuda será apreciada.

EDITAR:

La solución de Ed''ka funciona pero de una manera completamente diferente. Todavía estoy tratando de entender cuándo podemos ejecutar un programa Prolog en el sistema de tipos, cuándo / por qué necesitamos escribir un algoritmo diferente para que funcione (como en la solución de Ed''ka), y cuándo / por qué no hay manera de Implementar un programa en el sistema de tipos de Haskell.

Tal vez pueda encontrar algunos consejos sobre esto después de leer "Diversión con dependencias funcionales".

Answer 1

Como @ stephen tetley ya señaló cuando GHC intenta hacer coincidir la declaración de la instancia, considera que solo la cabeza de la instancia (las cosas después de =>) ignora por completo el contexto de la instancia (cosas antes de =>), una vez que se encuentra la instancia inequívoca, intenta hacer coincidir el contexto de la instancia . Su primer ejemplo problemático claramente tiene duplicación en el encabezado de la instancia, pero se puede arreglar fácilmente reemplazando dos instancias en conflicto con una instancia más general:

instance (Greaterthan a b r)  => Greaterthan (Succ a) (Succ b) r

El segundo ejemplo, sin embargo, es mucho más difícil. Sospecho que para que funcione en Haskell necesitamos una función de nivel de tipo que pueda producir dos resultados diferentes dependiendo de si una instancia específica está definida o no para los argumentos de un tipo en particular (es decir, si hay una instancia Child Name1 Name2 - recursively do algo con Name2 contrario devuelve BFalse ). No estoy seguro de si es posible codificar esto con tipos de GHC (sospecho que no lo es).

Sin embargo, puedo proponer una "solución" que funciona para un tipo de entrada ligeramente diferente: en lugar de implicar la ausencia de una parent->child (cuando no se define una instancia para tal par), podríamos codificar explícitamente todas las relaciones existentes utilizando listas de nivel de tipo . Entonces podemos definir la función de nivel de tipo Descend , aunque tiene que depender de la extensión OverlappingInstances muy temida:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
  FlexibleInstances, FlexibleContexts, TypeOperators,
  UndecidableInstances, OverlappingInstances #-}

data Anne
data Bridget
data Caroline
data Donna
data Emily
data Fred
data George

-- Type-level list
data Nil
infixr 5 :::
data x ::: xs

-- `bs` are children of `a`
class Children a bs | a -> bs

instance Children Anne (Bridget ::: Nil)
instance Children Bridget (Caroline ::: Donna ::: Nil)
instance Children Caroline (Emily ::: Nil)
-- Note that we have to specify children list for everyone
-- (`Nil` instead of missing instance declaration)
instance Children Donna Nil
instance Children Emily Nil
instance Children Fred (George ::: Nil)
instance Children George Nil

-- `or` operation for type-level booleans 
class OR a b bool | a b -> bool
instance OR BTrue b BTrue
instance OR BFalse BTrue BTrue
instance OR BFalse BFalse BFalse

-- Is `a` a descendant of `b`?
class Descend  a b bool | a b -> bool
instance (Children b cs, PathExists cs a r) => Descend a b r

-- auxiliary function which checks if there is a transitive relation
-- to `to` using all possible paths passing `children`
class PathExists children to bool | children to -> bool

instance PathExists Nil a BFalse
instance PathExists (c ::: cs) c BTrue
instance (PathExists cs a r1, Children c cs1, PathExists cs1 a r2, OR r1 r2 r)
    => PathExists (c ::: cs) a r

-- Some tests
instance Show BTrue where
    show _ = "BTrue"

instance Show BFalse where
    show _ = "BFalse"

t1 :: Descend Donna Anne r => r
t1 = undefined -- outputs `BTrue`

t2 :: Descend Fred Anne r => r
t2 = undefined -- outputs `BFalse`

OverlappingInstances este caso, es necesario que las OverlappingInstances se PathExists ya que la segunda y la tercera instancia de PathExists pueden coincidir con el caso cuando los children no están en la lista vacía, pero GHC puede determinar una más específica en nuestro caso, dependiendo de si el encabezado de la lista es igual to argumento (y si lo es. significa que hemos encontrado el camino es decir, descendiente).

Answer 2

En cuanto al ejemplo de GreaterThan , no veo cómo introducir esos Boolean es un paso fiel al código Prolog original. Parece que está intentando codificar un sentido de decidibilidad en su versión de Haskell que no está presente en la versión Prolog.

Así que, en general, puedes hacer

{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
class Numeral a where

data Zero
data Succ a

instance Numeral Zero
instance (Numeral a) => Numeral (Succ a)

class (Numeral a, Numeral b) => Greaterthan a b where

instance (Numeral a) => Greaterthan Zero (Succ a)
instance (Greaterthan a b)  => Greaterthan (Succ a) (Succ b)

En realidad, con los tipos de datos , puedes escribirlo mejor (pero no puedo intentarlo ahora, ya que solo tengo ghc 7.2 instalado aquí):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}

data Numeral = Zero | Succ Numeral

class Greaterthan (a :: Numeral) (b :: Numeral) where

instance Greaterthan Zero (Succ a)
instance (Greaterthan a b)  => Greaterthan (Succ a) (Succ b)

Answer 3

Para la solución Ed''ka usted podría usar:

import Data.HList.TypeCastGeneric2
instance TypeCast nil Nil => Children a nil

en lugar de una instancia para cada persona que no tiene hijos.