Haskell's type system and logic programming - how to port Prolog programs to type level

Question

I'm trying to understand the relation between a logic programming language(Prolog in my case) and Haskell's type system.

I know both use unification and variables to find values(or types, in Haskell's type system) depending on relations. As an exercise to understand similarities and differences between them better, I tried to rewrite some simple prolog programs in Haskell's type level, but I'm having trouble with some parts.

First, I rewrote this simple prolog program:

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

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

as:

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

it works fine, but I couldn't extend it with this Prolog:

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

What I tried was this:

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

The problem with this code is that last two instances are causing fundep conflict. I can understand why, but it seems to me that it shouldn't be a problem since their guard parts(or whatever it's called it, I mean the (Greaterthan a b c) => part) are different, so that as and bs in last two insance declarations are actually different values and there are no conflicts.

---

Another program I tried to rewrite was this:

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).

(btw, examples are from Learn Prolog Now book)

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

And I'm getting "duplicate instances" error in last line. I think it's a similar problem, even if I have a different guard parts, I'm getting errors because body parts(I mean Descend a b parts) are the same.

So I'm looking for ways to port that Prolog programs to Haskell's type level, if possible. Any help will be appreciated.

EDIT:

Ed'ka's solution works but in a completely different way. I'm still trying to understand when we can run a Prolog program in type-system, when/why we need to write a different algorithm to make it work(like in Ed'ka's solution), and when/why there's no way to implemenet a program in Haskell's type-system.

Maybe I can find some pointers about this after reading "Fun With Functional Dependencies".

Daudet

See Thomas Hallgren's Fun With Functional Dependencies cse.chalmers.se/~hallgren/Papers/wm01.html if you haven't done already for some simple "type level prolog". You will always get duplicate instances for the last two lines because they are duplicates - GHC does not care that the constraints are different. – Laryngo

You might be interested in Mercury: Mercury is a functional logic programming language geared towards real-world applications. ... Mercury is a purely declarative logic language. It is related to both Prolog and Haskell. It features a strong, static, polymorphic type system, as well as a strong mode and determinism system. – Middleclass

You might be able to get a little further with associated type synonyms from -XTypeFamilies but I'm not sure how much. Interesting question – Pendant

@stephentetley thanks for the link but postscript download link isn't working, do you know any other mirrors ? – Daudet

@sinan - try Citeseer citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.7806 – Laryngo

When doing work like this, it's worth noting that the DataKinds language extension creates a kind for any defined ADT with types in that kind for each of the ADT's constructors, which you can reference using the KindSignatures extension. In this case, you therefore don't need classes and instances for Numeral and Boolean as you can use kinds instead. data Numeral=Zero|Succ Numeral and then your class declaration for Add becomes class Add (a :: Numeral) (b :: Numeral) (c :: Numeral) | a b -> c and so on. You actual don't need Boolean at all then, as you can use Prelude.Bool – Kimsey

Answer 1

As @stephen tetley has already pointed out when GHC tries to match instance declaration it considers only instance head (the stuff after =>) completely ignoring instance context (stuff before =>), once the unambiguous instance is found it tries to match instance context. Your first problematic example clearly has duplication in instance head but it can easily be fixed by replacing two conflicting instances with one more general instance:

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

The second example though is much harder one. I suspect that to make it work in Haskell we need a type-level function which could produce two different result depending on whether a specific instance is defined or not for a particular type arguments (i.e. if there is an instance Child Name1 Name2 - recursively do something with Name2 otherwise return BFalse). I am not sure if it is possible to code this with GHC types (I suspect it is not).

However, I can propose a "solution" which works for slightly different type of input: instead of implying absence of parent->child relation (when no instance is defined for such pair) we could explicitly encode all existing relationship using type-level lists. Then we can define Descend type-level function although it have to rely on much-dreaded OverlappingInstances extension:

{-# 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 is necessary here since 2nd and 3rd instances of PathExists can both match the case when children is not empty list but GHC can determine more specific one in our case depending whether the head of the list is equal to to argument (and if it is it means we have found the path i.e. descendant).

Raw

Answer 2

As for the GreaterThan example, I don't see how introducing those Booleans is a step faithful to the original Prolog code. It seems you are trying to encode a sense of decidability in your Haskell version that is not present in the Prolog version.

So all in all, you can just do

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

Actually with data kinds, you can write it nicer (but I can't try it now, as I only have ghc 7.2 installed here):

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

Papiamento

without help of FunDeps or something similar, I don't think you can run any type-level functions. in your code, how does Greaterthan class help us decide if parameters are in defined relationship ? I think your typeclass should have the body of Greaterthan a b something | a b -> something to be able to actually use a and b to derive something. in my case this something was r which was a Boolean type. – Daudet

@sinan: That's what was meant by "encode a sense of decidability". This expresses a constraint, not a usable function as such--it helps you decide by giving a compiler error if the constraint is not satisfied. Brings back fond memories of running a large program in prolog and getting only a completely unhelpful "no" in reply. – Lautrec

Answer 3

For Ed'ka solution you could use:

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

instead of one instance for each person who has no children.

Salema

@sinan: Do note that HList is a bit dated at this point, as newer GHC extensions provide features directly which HList implements from scratch. Also, I'd suggest reading the content at okmij.org/ftp rather than attempting to make sense of HList's source. – Lautrec

I can't find that module in the HList library's documentation. Can you describe where to find it and give more detail of what it does? I've tried reading through the summary of Oleg's web site (as linked by @C.A.McCann above) but there is a lot of information there and can't find anything about this specific typeclass. – Kimsey

Answer 4

I've played around with the second problem, and here is what I found out. It is possible to formulate the problem "a-la" Prolog, but some caveats apply. One of those caveats is that Descend doesn't actually have any functional dependencies between arguments, it's a binary predicate, not a unary function.

To begin with, let me show the code:

{-# LANGUAGE FunctionalDependencies
           , FlexibleInstances
           , UndecidableInstances
           , NoImplicitPrelude
           , AllowAmbiguousTypes
           #-}

data Anne
data Bridget
data Caroline
data Donna
data Emily

class Child a b | a -> b

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

----------------------------------------------------

data True -- just for nice output

class Descend a b where descend :: True

instance {-# OVERLAPPING #-} Descend a a
instance (Child a b, Descend b c) => Descend a c

(you can test this in GHCi by enabling :set -XTypeApplications and running something like :t descend @Anne @Caroline and :t descend @Caroline @Anne)

So, this mostly follows the Prolog example, with one important difference: instead of descend(X,Y) :- child(X,Y) we have

instance {-# OVERLAPS #-} Descend a a

I will explain momentarily why that is, but first I will explain what it changes: basically, the Descend relation becomes reflective, i.e. Descend a a is true for all a. This is not the case with the Prolog example, where the recursion terminates one step earlier.

Now for why that is. Consider how GHC implements type variable substitutions during type instance resolution: it matches the instance head, unifying the type variables, then checks the instance constraints. Hence, for example, Descend Anne Caroline will be resolved with the following sequence:

1. First Descend Anne Caroline is matched against Descend a c, conveniently a=Anne, c=Caroline
2. Hence, we look up instances Child Anne b and Descend b Caroline.
3. Generally, GHC would give up here since it wouldn't know what b means. But since in Child b is functionally dependent on a, Child Anne b is resolved to Child Anne Bridget, hence b=Bridget, and we try to resolve Descend Bridget Caroline.
4. Descend Bridget Caroline is again matched against Descend a c, a=Bridget, c is yet again Caroline.
5. Lookup Child Bridget b, which resolves to Child Bridget Caroline. Then try to resolve Descend Caroline Caroline.
6. Descend Caroline Caroline is matched with overlapping instance Descend a a and the process terminates.

So, GHC actually can't stop iterating early due to how instances are matched.

That said, if we replace Child with a closed type family, it becomes workable:

{-# LANGUAGE TypeFamilies
           , FunctionalDependencies
           , FlexibleInstances
           , UndecidableInstances
           , TypeOperators
           , NoImplicitPrelude
           , AllowAmbiguousTypes
           , ScopedTypeVariables
           #-}

data Anne
data Bridget
data Caroline
data Donna
data Emily

data True
data False

type family Child' a where
 Child' Anne     = Bridget
 Child' Bridget  = Caroline
 Child' Caroline = Donna
 Child' Donna    = Emily
 Child' a        = False

class Child a b | a -> b

instance (Child' a ~ b) => Child a b

----------------------------------------------------

class Descend' a b flag
class Descend a b where descend :: True

data Direct
data Indirect

type family F a b where
  F False a = Direct
  F a a = Direct
  F a b = Indirect

instance (Child' a ~ c) => Descend' a c Direct
instance (Child a b, Descend' b c (F (Child' b) c))
  => Descend' a c Indirect
instance (Descend' a b (F (Child' a) b))
  => Descend a b

The dance with Descend' is just to be able to overload instance selection based on context, as described in https://wiki.haskell.org/GHC/AdvancedOverlap. The main difference is we can apply Child' several times in order to "look ahead".

Kumasi