On Mon, Oct 31, 2011 at 6:52 PM, Paterson, Ross
If you require the circuit to be parametric in the value types, you can limit the types of function you can pass to arr to simple plumbing. See the netlist example at the end of my "Fun of Programming" slides ( http://www.soi.city.ac.uk/~ross/papers/fop.html).
That's a neat trick, Ross! It seems really similar to using parametricity to recover the insides of lambdas in PHOAS metaprogramming: -- HOAS expression language data Expr (v :: * -> *) a where Ap :: Expr v (a -> b) -> Expr v a -> Expr v b Var :: v a -> Expr v a Lam :: (v a -> Expr v b) -> Expr v (a -> b) -- some expressions that are paremetric in the variable type ex_id :: Expr v (a -> a) ex_id = Lam $ \x -> Var x ex_const :: Expr v (a -> b -> a) ex_const = Lam $ \x -> Lam $ \y -> Var x -- a print function that relies on parametricity to expose the insides of the functions inside "Lam" printExpr :: (forall v. Expr v a) -> String printExpr e = pe_helper vars 0 e "" where vars = map (:[]) ['a' .. 'z'] ++ map (\n -> "t" ++ show n) [1..] prec_lam = 1 prec_ap = 2 newtype VarName a = VarName String pe_helper :: [String] -> Expr VarName a -> Int -> ShowS pe_helper fv prec (Var (VarName s)) = showString s pe_helper fv prec (Ap x y) = showParen (prec > prec_ap) (pe_helper fv prec_ap x . showString " " . pe_helper fv (prec_ap+1) y) pe_helper (v:fv) prec (Lam k) = showParen (prec > prec_lam) (showString "\" . showString v . showString " -> " . pe_helper fv prec_lam e) where e = k (VarName v) -- some test cases test1 = printExpr ex_const -- "\a -> \b -> a" test2 = printExpr (ex_id `Ap` ex_const) -- "(\a -> a) (\a -> \b -> a)"