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>