[Haskell-cafe] Re: Sorting Types

[Casey McCann]

On Tue, Apr 27, 2010 at 10:20 AM, John Creighton <johns243a at gmail.com> wrote:
>> I was wondering if it is possible to sort types in hakell and if so what
>> language extension I should use.

There are multiple ways that some manner of ordering could be defined
on types. A structural definition is one method; ordering Peano
numerals is a simple example, but the same idea applies more generally
to examining the size/depth/etc. of nested constructors. Another
option is defining an explicit ordering on some specified group of
types; this allows greater flexibility at the cost of needing to
manually add types to the ordering.

At any rate, both involve fairly straightforward type-level
programming, possible (and in fact rather easy) to accomplish using
functional dependencies with overlapping and undecidable instances. A
more limited set of extensions is probably viable for some types of
ordering, possibly at the expense of some verbosity or difficulty.
Unfortunately I'm not very practiced with type families, so I'm not
sure how it translates to those; the lack of overlapping instances
makes some things awkward or impossible using type families, alas.

>> I get the following error:
>>
>>   Illegal type synonym family application in instance: And a (LT a i)
>>   In the type synonym instance declaration for 'Sort'

Well, as it says, type synonym instances can't be used as parameters
to type synonym instances. What constitutes a legal instance
declaration is described in the GHC user's guide, section 7.7.2.2., if
you want clarification.

To keep this from being too much doom and gloom, here's a
quick-and-dirty example of one way to define an arbitrary explicit
ordering on a group of types, that might give you some ideas.

First, all the usual extensions that announce: "Warning! We're about
to abuse the type system!"

> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE OverlappingInstances #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FunctionalDependencies #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE FlexibleContexts #-}

My preferred type-level booleans, terse yet friendly.

> data Yes = Yes deriving (Show)
> data No = No deriving (Show)

We'll need some very simple type-level lists. Nothing fancy here.

> data Nil = Nil deriving (Show)
> infixr 5 :*:
> data a :*: b = a :*: b deriving (Show)

Four possible results for a comparison. Note the presence of
"Unordered", as the comparisons are defined only on an explicit group
of types. The TypeOrdering class is used only to convert type-level
results to equivalent values, for easier inspection.

> data Less = Less deriving (Show)
> data Equal = Equal deriving (Show)
> data Greater = Greater deriving (Show)
> data Unordered = Unordered deriving (Show)
> class TypeOrdering t where toOrdering :: t -> Maybe Ordering
> instance TypeOrdering Less where toOrdering _ = Just LT
> instance TypeOrdering Equal where toOrdering _ = Just EQ
> instance TypeOrdering Greater where toOrdering _ = Just GT
> instance TypeOrdering Unordered where toOrdering _ = Nothing

Now for the meaty bits. The type compare function takes three
arguments: a type-level list that specifies the ordering to use, and
two types to compare. The list is treated as a comprehensive
least-to-greatest enumeration of the ordered types; if either type
argument isn't in the list, the result will be Unordered.

The general structure is just simple recursion, obfuscated by
implementation details of type-level programming. Roughly speaking,
conditionals in type-level functions are most conveniently written by
calling another type function whose instances are determined by the
conditional expression; this is to avoid having GHC evaluate both
branches of the conditional, which would lead to unnecessary
computation at best and compiler errors at worst.

To start with, if the list is empty, the types are unordered;
otherwise, we compare both types to the head of the list and branch on
the results.

> class Compare ord x y r | ord x y -> r where
>     tComp :: ord -> x -> y -> r
>     tComp = undefined
> instance (
>     TypeEq o x bx,
>     TypeEq o y by,
>     Comp' bx by ord x y r
>     ) => Compare (o :*: ord) x y r
> instance Compare Nil x y Unordered
>
> class Comp' bx by ord x y r | bx by ord x y -> r

If both types and the list head are all equal, the result is obviously Equal.

> instance Comp' Yes Yes ord x y Equal

If neither is equal to the list head, recurse with the list tail.

> instance (Compare ord x y r) => Comp' No No ord x y r

If one of the types is equal to the list head, that type will be the
lesser if an ordering exists at all. We select the optimistic result
and call another function with the type we didn't find.

> instance (Comp'' ord y Less r) => Comp' Yes No ord x y r
> instance (Comp'' ord x Greater r) => Comp' No Yes ord x y r

If the list is empty, the result is unordered, as before. Otherwise,
we compare the type with the list head and branch with yet another
function.

> class Comp'' ts t o r | ts t o -> r
> instance Comp'' Nil t o Unordered
> instance (TypeEq x t b, Comp''' b xs t o r) => Comp'' (x :*: xs) t o r

If the type and list head are equal, we return the optimistic result
from above (which was chosen based on which parameter was found
first). Otherwise, recurse on the list tail with the previous
function.

> class Comp''' b ts t o r | b ts t o -> r
> instance Comp''' Yes ts t o o
> instance (Comp'' ts t o r) => Comp''' No ts t o r

Now, to demonstrate, a few types to consider.

> data Cat = Cat deriving (Show)
> data Dog = Dog deriving (Show)
> data Fish = Fish deriving (Show)
> data Whale = Whale deriving (Show)

Two different orderings on the types we just defined:

> alphabetical = Cat :*: Dog :*: Fish :*: Whale :*: Nil
> size = Fish :*: Cat :*: Dog :*: Whale :*: Nil

Here's a function that does a comparison. Try it out!

> typeCompare :: (Compare ord x y r, TypeOrdering r) => ord -> x -> y -> Maybe Ordering
> typeCompare ord x y = toOrdering $ tComp ord x y

Using the Compare type function above, it should be straightforward to
define more complicated computations; for instance, sorting a list of
heterogeneous types, or building a type-level binary search tree.

And as a quick addendum, here's a bit of very useful type
metaprogramming needed to make the above code work. These well-known
type classes are, of course, borrowed from Oleg; so let's be careful
to return them in good condition without any dents or scratches.

> class TypeEq' () x y b => TypeEq x y b | x y -> b
> instance TypeEq' () x y b => TypeEq x y b
> class TypeEq' q x y b | q x y -> b
> class TypeEq'' q x y b | q x y -> b
>
> instance TypeCast b Yes => TypeEq' () x x b
> instance TypeEq'' q x y b => TypeEq' q x y b
> instance TypeEq'' () x y No
>
> class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
> class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
> class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
> instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
> instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
> instance TypeCast'' () a a where typeCast'' _ x  = x

Hope that helps,

- C.