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? Thanks, Ian
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?
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?
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?
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?
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?
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?
Ian,
This requires dynamic typing using Data.Dynamic (for application) and
Data.Typeable (to do the typing). Namely, you are asking for the
"dynApply" function:
---- START CODE
import Data.Dynamic
import Data.Typeable
import Control.Monad
maybeApp :: (Typeable a, Typeable b, Typeable c) => a -> b -> Maybe c
maybeApp a = join . fmap fromDynamic . dynApply (toDyn a) . toDyn
---- END CODE
In the above we obtain representations of your types in the form of
"Dynamic" data types using toDyn. Then, using dynApply, we get a
value of type "Maybe Dynamic", which we convert back into a "c" type
with fromDynamic. The "join" is just there to collapse the type from
a "Maybe (Maybe c)" into the desired type of "Maybe c".
Cheers,
Thomas
P.S.
If I totally misunderstood, and you want static typing then you just
need to realize you _don't_ want types "a" and "b" (fully polymorphic)
but rather types (b -> c) and b:
apply :: (b -> c) -> b -> c
apply a b = a b
But this seems rather silly, so I hope you were looking for my first answer.
On Wed, Jul 6, 2011 at 2:12 AM, Ian Childs
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?
Thanks, Ian
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
Henning Thielemann -
Ian Childs -
Thomas DuBuisson