Ian Childs wrote:
> 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.
Basically you have to write the deconstruct that takes
(TRepr a), the witness for typ
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
A
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, an
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 previ
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'
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
On Wed, 6 Jul 2011, Ian Childs wrote:
Suppose I have two terms s and t of type "a" and "b" respectively, and I want
to write a function that returns s applied to t if "a" is an arrow type of
form "b -> c", and nothing otherwise. How do i convince the compiler to
accept the functional applicat
