title: Haskell's type system and logic programming - how to port Prolog programs to type level
body: <p>I'm trying to understand the relation between a logic programming language(Prolog in my case) and Haskell's type system.</p>
  
  <p>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.</p>
  
  <p>First, I rewrote this simple prolog program:</p>
  
  <pre><code>numeral(0).
  numeral(succ(X)) :- numeral(X).
  
  add(0,Y,Y).
  add(succ(X),Y,succ(Z)) :- add(X,Y,Z).
  </code></pre>
  
  <p>as:</p>
  
  <pre><code>class Numeral a where
      numeral :: a
      numeral = u
  
  data Zero
  data Succ a
  
  instance Numeral Zero
  instance (Numeral a) =&gt; Numeral (Succ a)
  
  class (Numeral a, Numeral b, Numeral c) =&gt; Add a b c | b c -&gt; a where
      add :: b -&gt; c -&gt; a
      add = u
  
  instance (Numeral a) =&gt; Add a Zero a
  instance (Add x y z) =&gt; Add (Succ x) (Succ y) z
  </code></pre>
  
  <p>it works fine, but I couldn't extend it with this Prolog:</p>
  
  <pre><code>greater_than(succ(_),0).
  greater_than(succ(X),succ(Y)) :- greater_than(X,Y).
  </code></pre>
  
  <p>What I tried was this:</p>
  
  <pre><code>class Boolean a
  data BTrue
  data BFalse
  instance Boolean BTrue
  instance Boolean BFalse
  
  class (Numeral a, Numeral b, Boolean r) =&gt; Greaterthan a b r | a b -&gt; r where
      greaterthan :: a -&gt; b -&gt; r
      greaterthan = u
  
  instance Greaterthan Zero Zero BFalse
  instance (Numeral a) =&gt; Greaterthan (Succ a) Zero BTrue
  instance (Numeral a) =&gt; Greaterthan Zero (Succ a) BFalse
  instance (Greaterthan a b BTrue)  =&gt; Greaterthan (Succ a) (Succ b) BTrue
  instance (Greaterthan a b BFalse) =&gt; Greaterthan (Succ a) (Succ b) BFalse
  </code></pre>
  
  <p>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 <code>(Greaterthan a b c) =&gt;</code> part) are different, so that <code>a</code>s and <code>b</code>s in last two insance declarations are actually different values and there are no conflicts.</p>
  
  <hr>
  
  <p>Another program I tried to rewrite was this:</p>
  
  <pre><code>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).
  </code></pre>
  
  <p>(btw, examples are from <a href="http://www.learnprolognow.org" rel="noreferrer">Learn Prolog Now</a> book)</p>
  
  <pre><code>data Anne
  data Bridget
  data Caroline
  data Donna
  data Emily
  
  class Child a b | a -&gt; b where
      child :: a -&gt; b
      child = u
  
  instance Child Anne Bridget
  instance Child Bridget Caroline
  instance Child Caroline Donna
  instance Child Donna Emily
  
  class Descend a b | b -&gt; a where
      descend :: b -&gt; a
      descend = u
  
  instance (Child a b) =&gt; Descend a b
  instance (Child a c, Descend c b) =&gt; Descend a b
  </code></pre>
  
  <p>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 <code>Descend a b</code> parts) are the same.</p>
  
  <p>So I'm looking for ways to port that Prolog programs to Haskell's type level, if possible. Any help will be appreciated.</p>
  
  <p>EDIT:</p>
  
  <p>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.</p>
  
  <p>Maybe I can find some pointers about this after reading "Fun With Functional Dependencies".</p>