[Haskell-cafe] do we need types?

[Jason Dusek]

  This reminds me of an email posted to this list long ago
  by Luke Palmer, describing a use of records-as-interfaces
  in Agda.

--
Jason Dusek


---------- Forwarded message ----------
From: Luke Palmer <lrpalmer at gmail.com>
Date: 2009/12/29
Subject: Re: [Haskell-cafe] Alternatives to type classes.
To: Jason Dusek <jason.dusek at gmail.com>
Cc: haskell <haskell-cafe at haskell.org>


On Tue, Dec 29, 2009 at 6:22 PM, Jason Dusek <jason.dusek at gmail.com> wrote:
>  Consider the real numbers. They "are" a group. We have an
>  identity element `0', inverses and closure under the associative
>  operation `+'.
>
>    Group+ = (+, 0, -1 * _)
>
>  They are another group, too -- the group with `*':
>
>    Group* = (*, 1, 1 / _)

Ignoring 0 for sake of discussion.

>  This seems like a real problem with the whole notion of
>  typeclasses -- we can't really say a set/type "is" its
>  extension with some new operations.
>
>  One road to go on this is to make every extension of the set
>  with new ops a different type; but that seems really horribly
>  inconvenient. I wonder what approaches have been tried here?

I consider typeclasses a happy notational medium.  They are not
perfect, they miss some cases, but they are pretty good.

For full generality at the expense of some verbosity, I like Agda's
solution pretty well.  Agda allows you to "open" a record into a
scope.

record Group (a : Set) where
 field
   _+_ : a -> a -> a
   -_ : a -> a
   0 : a

conj : {a : Set} -> Group a -> a -> a -> a
conj g x y = x + y + (-x)
   where open g

Maybe I even got the syntax right :-P

The cool thing is that you can use this for the invariant-keeping
property of typeclasses, too.  Eg. Data.Map relies on the fact that
there is at most one Ord instance per type.  By parameterizing the
module over the Ord record, we can do the same:

record Ord (a : Set) where ...

module MapMod (a : Set) (ord : Ord a) where
 Map : b -> Set
 Map = ...
 insert : {b : Set} -> a -> b -> Map b -> Map b
 insert = ...
 ...

So we have the liberty of being able to use different Ord instances,
but different Ord instances give rise to different Map types, so we
can not violate any invariants.

You can do something similar in Haskell using an existential type,
although it is very inconvenient:

data Ord a = ...
data MapMod map a b = MapMod { empty :: map a b, insert :: a -> b ->
map a b -> map a b, ... }

withMap :: Ord a -> (forall map. MapMod map a b -> z) -> z
withMap ord f = f ( {- implement MapMod here, using ord for ordering }- )

Then you could use maps on different Ords for the same type, but they
could not talk to each other.

Some syntax sugar could help the Haskell situation quite a lot.