Peano's Axioms Part III: Making use of Haskell's Powerful Polymorphism

This time, we'll be looking at making use of the polymorphic capabilties of Haskell's type system.

In Haskell, Polymorphism is provided via type variables. That is, you may have a function

foo :: (a -> b) -> [a] -> [b]

which requires a function of any type to any other type, and a list of elements of the first type, and it returns a list of elements of the second type. Most people call this function map, though it can represent others.

So in addition to getting the functions defined in the typeclass, we get all the prelude functions with variable type signatures.

But wait- theres more. When we define certain types of functions, we often want to limit the scope of the function to only operate on certain variables. Like defining an instance of an interface in Java, we can specify a "scope" (though thats an abuse of the term) for a type variable. As in the following:

foo2 :: Ord a => a -> a -> a

Here, we state that a must be an instance of the typeclass Ord (and by inheritance, an instance of Eq too.) So now we know that foo2 takes two comparable elements and returns a comparable element.

Polymorphism is nothing new to any language. However, I think that Haskell really has an advantage not in the area of semantics, which are pretty much uniform -- at least in the case of polymorphism. I think that Haskell's advantage is in the syntax of polymorphism. Type signatures are easily wonderfully simple ways to express polymorphism. Both this basic kind of polymorphism (called rank-1 polymorphism), as well as higher order polymorphism (rank-2, rank-3, rank-n).

The point of this post is to show the rich library of polymorphic functions which become available with just a few (I think we're up to 7, one derived, 6 implemented) type classes. This, as always, is a literate file, just cut and paste to a .lhs and run


$> ghci .lhs


> module Peano2 (Nat(..)) where
> import Peano
> import Data.Ratio

==============================================================
Continuing on which defining math in terms of Peano's axioms
==============================================================

Last time I noted that we'd be working on exp, div, mod, and some other
higher-level functions. I also mentioned that we "sortof" got exp for free, in
that

S(S(S(Z)))^k,

where k is an integer, works fine, but what if we k be a natural. we'll notice
readily that this will fail, with the error that theres no instance of
Integral Nat.

Why is that a problem? because (^) isn't in Num, its defined elsewhere, its
signature is

(^) :: (Num a, Integral b) => a -> b -> a

Okay, so now what we should do is define Nat to be an Integral Type. So, lets go
for it.


=======================================

so, for Integral, we need quot, rem, and toInteger. We have the last of these, from the last time. Its quot and rem that we need. So, how do we define these?

well, we know that quot and rem are (effectively) just mod and div, in fact, not having negative numbers means that they are exactly the same. Lets then realize that mod is just repeated subtraction until we hit modulus > remnant. further, we relize that div is just the same, but the count of times we subtracted till we met that condition.

> quotNat :: Nat -> Nat -> Nat
> quotNat k m 
>    | k == m       = 1
>    | k < m        = 0
>    | otherwise    = 1 + (quotNat (k-m) m)

> remNat :: Nat -> Nat -> Nat
> remNat k m 
>    | k == m       = 0
>    | k < m        = k
>    | otherwise    = remNat (k-m) m

> quotRemNat     :: Nat -> Nat -> (Nat, Nat)
> quotRemNat k m = ((quotNat k m), (remNat k m))

now, we just instantiate integral

> instance Integral Nat where
>    toInteger = ntoi
>    quotRem = quotRemNat
>    -- this fixes a problem that arises from Nats not having
>    -- negative numbers defined.
>    divMod = quotRemNat

=======================================

but now we need to instantiate Enum and Real, oh my. Lets go for Enum first.

Enum requires just toEnum and fromEnum, thats pretty easy, to and from enum are just to and from Integer, which we have.

> instance Enum Nat where
>    toEnum = integerToNat
>    fromEnum = natToInteger 

Real is actually relatively easy, we're just projecting into a superset of the
Naturals, notably, the Rationals, so we do this simply by pushing the value
into a ratio of itself to 1, that is

toRational S(S(S(S(Z)))) ==> S(S(S(S(Z)))) % 1

> instance Real Nat where
>    toRational k = (ntoi k) % 1

=======================================

Next time, we'll go for primes.

oh- and by the way, pushing Nat into Integral gave us lots of neat things, notably even/odd, gcd/lcm, the ability to do ranges like [(Z)..], and all the appropriate functions that go with that.

So far, I've spent about 1 hour making all this work, you can imagine how this speed could be useful if you have defined your problem as having certain properties. Type classes are an extremely powerful tool, which can help make your code both clean, as well as powerful. In one hour, I've managed to build up a simple bit of code, based on some fairly primitive axioms, and create a huge amount of powerful math around it.

Imagine if you could define these same relations around data? What if you were able to define strings as having properties of numbers, heres an Idea:

Imagine you have some strings, you can define the gcd of two strings as the least common substring of two strings. If you can sensically define the product of two strings, then you can get a concept of lcm as well. Granted, the may not be the best example. But you can just imagine the power you can push into your data by defining an arithmetic, (not even an algebra!) on them. Imagine creating an arithmetic of music (been done, sortof, check out Haskore) or pictures? I use
arithmetic,because what I'm implementing here is only a little peice of the power you can instill. _This_ is why Haskell is powerful. Not because its purely functional, not even because its lazy. It's the _math_ that makes Haskell capable of doing this. The type theory upon which Haskell rests makes Haskell powerful.

Remember, next time, Primes and Totients and Number Theory, and a datatype
representing the Integers,
Oh my!