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

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 `a`

s and `b`

s 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".

Solution

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

- How can I refactor from error to an ExceptT?
- How can I generate a random sequence of elements from a list in Haskell?
- Problem with quantified types and pattern matching
- Why is the `unicode-show` package necessary?
- Get sum of int or integer in Haskell
- Java 8: streams and the Sieve of Eratosthenes
- Can iterate be written with a fold?
- Haskell function with data pattern match and second argument gives Equations have different numbers of arguments
- How to use (->) instances of Monad and confusion about (->)
- Trouble understanding Haskell type unification with a nested `fmap`
- why ghc does not support PIE and Full RelRO in linux?
- Controlling Wai logger messages
- How do Haskell compilers decide whether to allocate on the heap or the stack?
- How can date/time format of Yesod logger be configured?
- In Haskell's Turtle library, how to copy a file, but preserve the file date
- Could not deduce (Semigroup (TimedEvents a))
- Instance of class with Data family yielding error "Couldn't match expected type"
- Is there a way to get a Haskell setup on Windows without an installation? (Copy + paste)
- Haskell parse error on input `<-'
- Inline assembly in Haskell
- How do I deal with arbitrary length tuple to build up a complex SQL query for Haskell's postgresql-simple's query function?
- Extract liftIO and runSql in separate function (Haskell)
- How to query NodeJS stream 'meta data'?
- Building multiple executables in the default Haskell Stack project
- Take elements of a list up to and including the first value that satisfies some predicate in Haskell
- How are Hackage package names mapped to 'cabal install' names?
- Insert entity into DB with manually created foreign key in Persistent library (Haskell)
- couldn´t match type 'IO´ with ´[]` inside a do
- Why doesn't contravariance apply in certain cases like [b] → Int < a → Int
- How does the Haskell compiler handle the 'where' statement?