127 lines
4.3 KiB
Markdown
127 lines
4.3 KiB
Markdown
---
|
|
title: Typeclasses are Basically Logic Programming
|
|
date: 2021-06-28T17:11:38-07:00
|
|
expirydate: 2021-06-28T17:11:38-07:00
|
|
draft: true
|
|
description: "In this post, we explore the connection between typeclasses and logic programming."
|
|
tags: ["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`.
|
|
|
|
```Haskell
|
|
class Show a where
|
|
show :: a -> String
|
|
```
|
|
|
|
An instance of `Show` may look as follows:
|
|
|
|
```Haskell
|
|
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:
|
|
|
|
```Haskell
|
|
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:
|
|
|
|
```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.
|
|
|
|
```Haskell
|
|
show () = "()"
|
|
show [()] = "[()]"
|
|
show [[()],[()]] = "[[()],[()]]"
|
|
show [[[()],[()]]] = "[[[()],[()]]]"
|
|
...
|
|
```
|
|
|
|
A similar principle applies to tuples, `(a,b)`. Here's the Haskell instance:
|
|
|
|
```Haskell
|
|
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`:
|
|
|
|
```Haskell
|
|
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`.
|