[Haskell-cafe] function terms

[Ian Childs]

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?