Sun Oct 2 18:44:03 EDT 2011
Inductive inputs / outputs
From the LLVM code:
-- An alias for pairs to make structs look nicer
type (:&) a as = (a, as)
(&) :: a -> as -> a :& as
a & as = (a, as)
This is useful as it's possible to inductively build function types
with multipe inputs and outputs. See for a 4 in, 4 out function.
(* -> (* -> (* -> (* -> (* :& (* :& (* :& (* :& ()))))))))
Does it also exist in the non-curried variant? It seems that in that
case it's no longer a sequence, but a tree split by the `->' type
(* :& (* :& (* :& (* :& ())))) -> (* :& (* :& (* :& (* :& ()))))
Why is induction (linear list structure) useful? It allows the
definition of an enumerable set of type classes, starting with the
base case and working up through induction, just like one would write
recursive functions on recursive types.
It doesn't seem that functionally the non-curried case is less
powerful, just that it's more of a hassle to deconstruct the type in
the inductive rule.
See next post for example of how a function arity can be obtained from
a function type using a type class and 3 instances. Once base case ()
and one for each induction.