On Tue, Apr 27, 2010 at 10:20 AM, John Creighton johns2...@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 |
