Term a is meant to be the simply-typed lambda-calculus as a GADT.
Then given two terms App (App "=" l1) r1, and App (App "=" l2) r2, I
want to form App (App "=" (App l1 l2)) (App r1 r2), but as you can
see this will only work if the types of l1 and l2, and r1 and r2,
match as detailed previously. does that make sense?
On 6 Jul 2011, at 10:48, Henning Thielemann wrote:
On Wed, 6 Jul 2011, Ian Childs wrote:
Yes they are Haskell expressions - I called them terms because
actually they
are GADTs of type Term a and Term b. I can't use type 'b -> c' as
they are
part of a larger pattern.
I have a function that returns a witness to 's :: Term a' and
't :: Term b'
having the same type, if they do, but I am wondering how to extend
this to
the first argument of an arrow type.
Can you give us a bit more (but not too much) code in order to show
the
problem?
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
