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. Thanks On 6 Jul 2011, at 10:23, Henning Thielemann wrote:
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 application only in the correct instance?
Why can't 's' simply have type 'b -> c'? With "term" do you mean a Haskell expression?