argument permutation and fundeps

[C T McBride]

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