Sorry, that should be (Const "="). The GADT is defined as follows:
data Var a where
MkVar :: (GType a) => String -> Var a
data LTerm a where
Var :: (GType a) => Var a -> LTerm a
Const :: (GType a) => String -> LTerm a
(:.) :: (GType a, GType b) => LTerm (a -> b) -> LTerm a -> LTerm b
Abs :: (GType a, GType b) => Var a -> LTerm b -> LTerm (a -> b)
infixl 6 :.
(here i have used :. instead of App so that it is easier to read). I
had to restrict types to the class (GType) of types that I have
instantiated for comparison.
On 6 Jul 2011, at 11:16, Henning Thielemann wrote:
On Wed, 6 Jul 2011, Ian Childs wrote:
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?
What is App? It looks like you apply it once to a string ("=") and
also to
terms(?) like l1, r1. How is the GADT defined?
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
