argument permutation and fundeps

[Ralf Hinze]

Dear Conor,

thanks for posing the `argument permutation' problem. I had several
hours of fun hacking up a solution that works under `ghci' (as Jeff
pointed out Hugs probably suffers from a bug). The solution is
relatively
close to your program, I only simplified the representation of the
`factorial numbers' that select a permutation.  The program is
attached below.

Here is a sample interaction (using `ghci -fglasgow-exts PermArg.lhs'):

PermArgs> :t pr
Int -> Bool -> Char -> [Char]
PPermArgs> :t perm (a0 <: a0 <: nil) pr
Int -> Bool -> Char -> [Char]
ermArgs> :t perm (a0 <: a1 <: nil) pr
Int -> Char -> Bool -> [Char]
PermArgs> :t perm (a1 <: a0 <: nil) pr
Bool -> Int -> Char -> [Char]
PermArgs> :t perm (a1 <: a1 <: nil) pr
Char -> Int -> Bool -> [Char]
PermArgs> :t perm (a2 <: a0 <: nil) pr
Bool -> Char -> Int -> [Char]
PermArgs> :t perm (a2 <: a1 <: nil) pr
Char -> Bool -> Int -> [Char]

Cheers, Ralf

---

> module PermArgs where

Natural numbers.

> data Zero                     =  Zero
> data Succ nat                 =  Succ nat

Some syntactic sugar.

> a0                            =  Zero
> a1                            =  Succ a0
> a2                            =  Succ a1
> a3                            =  Succ a2

Inserting first argument.

> class Insert nat a x y | nat a x -> y, nat y -> a x where
>     insert                    :: nat -> (a -> x) -> y
>
> instance Insert Zero a x (a -> x) where
>     insert Zero f             =  f
> instance (Insert nat a x y) => Insert (Succ nat) a (b -> x) (b -> y) where
>     insert (Succ n) f a       =  insert n (flip f a) 

Some test data.

> pr                            :: Int -> Bool -> Char -> String
> pr i b c                      =  show i ++ show b ++ show c

An example session (using `ghci -fglasgow-exts PermArg.lhs'):

PermArgs> :t insert a0 pr
Int -> Bool -> Char -> String
PermArgs> :t insert a1 pr
Bool -> Int -> Char -> String
PermArgs> :t insert a2 pr
Bool -> Char -> Int -> [Char]
PermArgs> :t insert a3 pr

No instance for `Insert (Succ Zero) Int String y'
arising from use of `insert' at <No locn>

Lists.

> data Nil                      =  Nil
> data Cons nat list            =  Cons nat list

Some syntactic sugar.

> infixr 5 <:

> (<:)                          =  Cons
> nil                           =  a0 <: Nil

Permuting arguments.

> class Perm list x y | list x -> y, list y -> x where
>     perm                      :: list -> x -> y
>
> instance Perm Nil x x where
>     perm Nil f                =  f
> instance (Insert n a y z, Perm list x y) => Perm (Cons n list) (a -> x) z where
>     perm (Cons d ds) f        =  insert d (\a -> perm ds (f a))

An example session (using `ghci -fglasgow-exts PermArg.lhs'):

PermArgs> :t perm (a0 <: a0 <: nil) pr
Int -> Bool -> Char -> [Char]
PermArgs> :t perm (a0 <: a1 <: nil) pr
Int -> Char -> Bool -> [Char]
PermArgs> :t perm (a1 <: a0 <: nil) pr
Bool -> Int -> Char -> [Char]
PermArgs> :t perm (a1 <: a1 <: nil) pr
Char -> Int -> Bool -> [Char]
PermArgs> :t perm (a2 <: a0 <: nil) pr
Bool -> Char -> Int -> [Char]
PermArgs> :t perm (a2 <: a1 <: nil) pr
Char -> Bool -> Int -> [Char]
PermArgs> :t perm (a2 <: a2 <: nil) pr
 
No instance for `Insert (Succ Zero) Int y y1'
arising from use of `perm' at <No locn>
 
No instance for `Insert (Succ Zero) Bool [Char] y'
arising from use of `perm' at <No locn>