blog-static/content/blog/typeclasses_are_logic.md

title	date	expirydate	draft	description	tags
Typeclasses are Basically Logic Programming	2021-06-28T17:11:38-07:00	2021-06-28T17:11:38-07:00	true	In this post, we explore the connection between typeclasses and logic programming.	Haskell Prolog

I recently spent some time playing around with the implementation of Haskell-like typeclasses in a toy functional language. In doing so I noticed how similar an implementation of a little logic programming language is to an implementation of type class search. Though this may be very well known, I thought I'd take some time to describe the similarities (and the differences).

Kicking off the Show

Let's begin with a very simple typeclass: Show. When I was a TA for my university's programming languages course, we mentioned this typeclass to the students, despite considering typeclasses as a whole to be a topic beyond our scope. Four our purposes, we can consider it to be a class with only one method: show.

class Show a where
    show :: a -> String

An instance of Show may look as follows:

instance Show () where
    show () = "()"

So far, we haven't done much: we let Haskell know of a typeclass Show, and also that () has an implementation of show. One might write this in Prolog as follows:

{{< codelines "Prolog" "typeclass-prolog/kb.pl" 1 1 >}}

Wait a moment, something was lost intranslation. What about show, and its implementation? We did not carry these over into Prolog. A truly equivalent formulation in Prolog would contain this information; however, for simplicity, {{< sidenote "right" "pretend-note" "we'll pretend that" >}} I'd argue that our little make-believe is morally correct. We can think of it in this way: to be allowed to write down the equivalent Prolog rule you need to provide all the required methods, and the proof that you provided them is recorded alongside the rule. A sort of entrance ticket, if you will. {{< /sidenote >}} the line of code above, and any further lines of code of that sort, are endowed with the implementation of all the required methods.

On to something more interesting. It's well known that if you can print the elements of a Haskell list, you can also print the list itself. The implementation looks something like this:

instance Show a => Show [a] where
    show l = "[" ++ intercalate "," (map show l) ++ "]"

We can't print just any list; for instance, [Int -> Bool] does not have a Show instance, because Int -> Bool itself does not have a show instance. This dependency is encoded in Prolog as follows:

{{< codelines "Prolog" "typeclass-prolog/kb.pl" 2 2 >}}

Implicit in both the Haskell instance and the Prolog rule is the "forall" quantifier: we have "for all types a, if Show a, then Show [a]", and "for all terms X, if show(X) holds, then show(list(X)) holds".

With only these two instances, what types can we print? Let's ask Prolog:

?- show(X).
X = unit ;
X = list(unit) ;
X = list(list(unit)) ;
X = list(list(list(unit))) ;
...

These correspond to () (naturally), [()], [[()]], and so on. Indeed, in Haskell, we'd be able to use show to turn values of these types (and only these types, assuming our two instances) into strings.

show () = "()"
show [()] = "[()]"
show [[()],[()]] = "[[()],[()]]"
show [[[()],[()]]] = "[[[()],[()]]]"
...

A similar principle applies to tuples, (a,b). Here's the Haskell instance:

instance (Show a, Show b) => Show (a, b) where
    show (a,b) = "(" ++ show a ++ "," ++ show b ++ ")"

The Prolog encoding is pretty much as one would expect:

{{< codelines "Prolog" "typeclass-prolog/kb.pl" 3 3 >}}

What of the superclasses?

We've explored few of the possibilities in the Haskell's typeclass system. For instance, there's another well-known typeclas, Ord:

class Eq a => Ord a where
    -- ...

This typeclass has a superclass: in order for some type a to have class Ord, it must also have class Eq. We haven't seen superclasses until now, but they are quite important to Haskell: Applicative is a superclass of Monad, which means you can use liftA2 and <*> on any monad. A typeclass having a superclass has two important implications for us.

First, we may not put down an instance of, say, Ord a, if we don't already have an implementation of Eq a.