Hi This is a long message, containing a program which makes heavy use of type classes with functional dependencies, and a query about how the typechecker treats them. It might be a bit of an effort, but I'd be grateful for any comment and advice more experienced Haskellers can spare the time to give me. Er, this ain't no undergrad homework... I'm a dependently typed programmer and a bit of an old Lisphead. What's common to both is that it's fairly easy to write `program reconstruction operations', like the argument permutation function (of which flip is an instance), specified informally thus: Given a permutation p on [1..n] and an n-ary function f, permArg p f x_p(1) .. x_p(n) = f x_1 .. x_n It's easy in Lisp because you can just compute the relevant lambda-expression for permArg p f syntactically, then use it as a program: of course, there's no type system to make sure your p is really a perm and your f has enough arguments. To give permArg a precise type, we have to compute an n-ary permutation of the argument types for an n-ary function space. That is, we need a representation of permutations p from which to compute (1) the type of the permutation function (2) the permutation function itself This isn't that hard with dependent types, because we can use the same kinds of data and program as easily at the level of types as we can at the level of terms. I'm relatively new to Haskell: what attracted me is that recent extensions to the language have introduced a model of computation at the type level via multi-parameter classes with functional dependencies. Although type-level Haskell programming is separate from, different to, and not nearly as powerful as term-level Haskell programming, it's still possible to do some pretty interesting stuff: here's permArg as a Haskell program... Although we can't compute with types over a data encoding of permutations, we can use type classes to make `fake' datatypes one level up. Here's a class representing the natural numbers. Each type in the class has a single element, which we can use to tell the typechecker which instance of the class we mean.
class Nat n
data O = O instance Nat O
data (Nat n) => S n = S n instance (Nat n) => Nat (S n)
Now, for each n in Nat, we need a class Fin n with exactly n instances. A choice of instance represents the position the first argument of an n-ary function gets shifted to. We can make Fin (S n) by embedding Fin n with one type constructor, FS, and chucking in a new type with another, FO.
class (Nat n) => Fin n x | x -> n
data (Nat n) => FO n = FO n instance (Nat n) => Fin (S n) (FO n)
data (Nat n,Fin n x) => FS n x = FS n x instance (Nat n,Fin n x) => Fin (S n) (FS n x)
The class Factorial n contains n! types---enough to represent the permutations. It's computed in the traditional way, but this time the product is cartesian...
class (Nat n) => Factorial n p | p -> n
instance Factorial O () instance (Factorial n p,Fin (S n) x) => Factorial (S n) (x,p)
The operation InsertArg n x r s, where x is in Fin (S n), takes an n-ary function type s and inserts an extra argument type r at whichever of the (S n) positions is selected by x. The corresponding function, insertArg permutes a (S n)-ary function in r -> s by flipping until the first argument has been moved to the nominated position. FS codes `flip the argument further in and keep going'; FO codes `stop flipping'.
class (Nat n,Fin (S n) x) => InsertArg n x r s t | x -> n, x r s -> t, x t -> r s where insertArg :: x -> (r -> s) -> t
instance (Nat n) => InsertArg n (FO n) r s (r -> s) where insertArg (FO _) f = f
instance (Nat n,Fin (S n) x,InsertArg n x r s t) => InsertArg (S n) (FS (S n) x) r (a -> s) (a -> t) where insertArg (FS _ x) f a = insertArg x (flip f a)
PermArg simply works its way down the factorial, performing the InsertArg indicated at each step. permArg is correspondingly built with insertArg.
class (Nat n,Factorial n p) => PermArg n p s t | p s -> t, p t -> s where permArg :: p -> s -> t
instance PermArg O () t t where permArg () t = t
instance (InsertArg n x r t u,PermArg n p s t) => PermArg (S n) (x,p) (r -> s) u where permArg (x,p) f = insertArg x (\r -> permArg p (f r))
This code is accepted by the Feb 2000 version of Hugs, of course with -98 selected. Let's look at some examples: the interesting thing is how the typechecker copes. Here's the instance of permArg which corresponds to flip Main> permArg (FS (S O) (FO O),(FO O,())) ERROR: Unresolved overloading *** Type : (InsertArg (S O) (FS (S O) (FO O)) a b c, InsertArg O (FO O) d e b, PermArg O () f e) => (a -> d -> f) -> c *** Expression : permArg (FS (S O) (FO O),(FO O,())) OK, I wasn't expecting that to work, because I didn't tell it the type of the function to permute: however, the machine did figure it out. Look at where it got stuck: I'd have hoped it would compute that e is f, and hence that b is d -> f, then possibly even that c is d -> a -> f. Isn't that what the functional dependencies say? On the other hand, if I tell it the answer, it's fine. Main> :t permArg (FS (S O) (FO O),(FO O,())) :: (a -> b -> c) -> b -> a -> c permArg (FS (S O) (FO O),(FO O,())) :: (a -> b -> c) -> b -> a -> c First, a nice little monomorphic function.
elemChar :: Char -> [Char] -> Bool elemChar = elem
There's no doubt about the type of the input, but this happens: Main> permArg (FS (S O) (FO O),(FO O,())) elemChar ERROR: Unresolved overloading *** Type : (InsertArg (S O) (FS (S O) (FO O)) Char a b, InsertArg O (FO O) [Char] c a, PermArg O () Bool c) => b *** Expression : permArg (FS (S O) (FO O),(FO O,())) elemChar What am I doing wrong? I hope my program says that c is Bool, and so on. Again, tell it the answer and it checks out: Main> :t (permArg (FS (S O) (FO O),(FO O,())) elemChar) :: [Char] -> Char -> Bool permArg (FS (S O) (FO O),(FO O,())) elemChar :: [Char] -> Char -> Bool Adding some arguments gives enough information about `the answer' to get rid of the explicit typing. Main> permArg (FS (S O) (FO O),(FO O,())) elemChar ['a','b','c'] 'b' True :: Bool It's the same story with arity 3... Main> :t permArg (FS (S (S O)) (FO (S O)),(FS (S O) (FO O),(FO O,()))) :: (a -> b -> c -> d) -> (c -> a -> b -> d) permArg (FS (S (S O)) (FO (S O)),(FS (S O) (FO O),(FO O,()))) :: (a -> b -> c -> d) -> c -> a -> b -> d Main> permArg (FS (S (S O)) (FO (S O)),(FS (S O) (FO O),(FO O,()))) foldl ERROR: Unresolved overloading *** Type : (InsertArg (S (S O)) (FS (S (S O)) (FO (S O))) (a -> b -> a) c d, InsertArg (S O) (FS (S O) (FO O)) a e c, InsertArg O (FO O) [b] f e, PermArg O () a f) => d *** Expression : permArg (FS (S (S O)) (FO (S O)),(FS (S O) (FO O),(FO O,()))) foldl Main> :t (permArg (FS (S (S O)) (FO (S O)),(FS (S O) (FO O),(FO O,()))) :: (a -> b -> c -> d) -> (c -> a -> b -> d)) foldl permArg (FS (S (S O)) (FO (S O)),(FS (S O) (FO O),(FO O,()))) foldl :: [a] -> (b -> a -> b) -> b -> b Main> permArg (FS (S (S O)) (FO (S O)),(FS (S O) (FO O),(FO O,()))) foldl [1,2,3] (+) 0 6 :: Integer So, am I failing to explain to Hugs why PermArg and InsertArg are programs, despite the explicit functional dependencies, or is the typechecker just not running them? It seems to be expanding PermArg's step case ok, but not executing the base case, leaving InsertArg blocked. Can anyone shed some light on the operational semantics of programming at the type level? Having, said all that, I'm really impressed that even this much is possible in Haskell. It's so nice to be able to write a type that says exactly what I mean. Cheers Conor