RE: [Haskell-cafe] checking types with type families
Martin Sulzmann, Jeremy Waznyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wazny:Jeremy.html, Peter J. Stuckeyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Stuckey:Peter_J=.html: A Framework for Extended Algebraic Data Types. FLOPS 2006http://www.informatik.uni-trier.de/%7Eley/db/conf/flops/flops2006.html#SulzmannWS06: 47-64 describes such a system, fully implemented in Chameleon, but this system is no longer maintained. Type families and Fundeps are equivalent in expressive power and it's not too hard to show how to encode one in terms of the other. Local constraints are an orthogonal extension. In terms of type inference, type families + local constraints and fundeps + local constraints pose the same challenges. Probably, Simon is refrerring to the 'unresolved' issue of providing a System F style translation for fundeps + local constraints. Apologies, Martin, you are quite right. Indeed, you were the first to teach me about implication constraints, which are the key to combining local constraints and functional dependencies. Chameleon implements such a system, using (I believe) the Constraint Handling Rule framework to solve the resulting constraints. However as you mention we could not figure out a good way to combine this approach to constraint solving with evidence generation, although it seems that in principle it should be possible. As you say Well, the point is that System FC is geared toward type families. The two possible solutions are (a) either consider fundeps as syntactic sugar for type families (doesn't quite work once you throw in overlapping instances), (b) design a variant System FC_fundep which has built-in support for fundeps. Why is FC is geared towards type families? It's not an accidental bias; it's more that I know how to do (a) and I don't know how to do (b). I'll write separately about the issue of overlap Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On Sat, Jul 3, 2010 at 4:28 PM, Dan Doel dan.d...@gmail.com wrote:
It's potentially not just a violation of intent, but of soundness. The
following code doesn't actually work, but one could imagine it working:
class C a b | a - b
instance C () a
-- Theoretically works because C a b, C a c implies that b ~ c
--
-- GHC says b doesn't match c, though.
f :: (C a b, C a c) = a - (b - r) - c - r
f x g y = g y
The funny part is that GHC eventually would decide they match, but not
until after it complains about (g y). For instance, if you do this:
f :: (C a b, C a c) = a - (b - r) - c - r
f x g y = undefined
...and load it into GHCi, it says the type is:
:t f
f :: (C a c) = a - (c - r) - c - r
As far as I can tell, type variables in scope simultaneously that
should be equal because of fundeps will eventually be unified, but
too late to make use of it without using some sort of type class-based
indirection. This can lead to interesting results when combined with
UndecidableInstances. For instance, consider the following:
class C a b c | a b - c where
c :: a - c - c
c = flip const
instance C () b (c, c)
f x = (c x ('a', 'b'), c x (True, False))
g :: (c, c) - (c, c)
g = c ()
This works fine: Because b remains ambiguous, the c parameters
also remain distinct; yet for the same reason, a effectively
determines c anyway, such that g ends up with the type (forall c.
(c, c) - (c, c)), rather than something like (forall c. c - c) or
(forall b c. (C () b c) = c - c). But if we remove the (seemingly
unused) parameter b from the fundep...
class C a b c | a - c where
...GHC now, understandably enough, complains that it can't match Char
with Bool. It will still accept this:
f x = c x ('a', 'b')
g x = c x (True, False)
...but not if you add this as well:
h x = (f x, g x)
Or even this:
h = (f (), g ())
On the other hand, this is still A-OK:
f = c () ('a', 'b')
g = c () (True, False)
h = (f, g)
Note that all of the above is without venturing into the
OverlappingInstances pit of despair.
I don't know if this is how people expect this stuff to work, but I've
made occasional use of it--introducing a spurious parameter in order
to have a fundep that uniquely determines a polymorphic type. Perhaps
there's a better way to do that?
- C.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On Wed, 23 Jun 2010 00:14:03 -0700, Simon Peyton-Jones simo...@microsoft.com
wrote:
I'm interested in situations where you think fundeps work and type families
don't. Reason: no one knows how to make fundeps work cleanly with local type
constraints (such as GADTs).
Simon,
I have run into a case where fundeps+MPTC seems to allow a more generalized
instance declaration than type families.
The fundep+MPTC case:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
class C a b c | a - b, a - c where
op :: a - b - c
instance C Bool a a where op _ = id
main = putStrLn $ op True done
In this case, I've (arbitrarily) chosen the Bool instance to be a no-op and
pass through the types. Because the dependent types are part of the
declaration header I can use type variables for them. I don't seem to have the
same ability with type families:
{-# LANGUAGE RankNTypes, TypeFamilies, UndecidableInstances #-}
class C a where
type A2 a
type A3 a
op :: a - A2 a - A3 a
instance {-forall a.-} C Bool where
type A2 Bool = {-forall a.-} a
type A3 Bool = A2 Bool
op _ = id
main = putStrLn $ op True done
I cannot get this to compile as above or with either of the existential
quantifications of a. The first example may be the more erroneous one because
the use of type variables would seem to violate the functional dependency
assertions, but GHC accepts it nonetheless.
Regards,
--
-KQ
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On Sat, Jul 3, 2010 at 3:32 AM, Kevin Quick qu...@sparq.org wrote:
On Wed, 23 Jun 2010 00:14:03 -0700, Simon Peyton-Jones
simo...@microsoft.com wrote:
I'm interested in situations where you think fundeps work and type
families don't. Reason: no one knows how to make fundeps work cleanly with
local type constraints (such as GADTs).
Simon,
I have run into a case where fundeps+MPTC seems to allow a more generalized
instance declaration than type families.
The fundep+MPTC case:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
class C a b c | a - b, a - c where
op :: a - b - c
instance C Bool a a where op _ = id
main = putStrLn $ op True done
In this case, I've (arbitrarily) chosen the Bool instance to be a no-op and
pass through the types. Because the dependent types are part of the
declaration header I can use type variables for them.
That's really weird. In particular, I can add this line to your code
without problems:
foo = putStrLn $ if op True True then done else .
but GHC complains about this one:
bar = putStrLn $ if op True True then op True done else .
fd.hs:14:0:
Couldn't match expected type `Bool' against inferred type `[Char]'
When using functional dependencies to combine
C Bool [Char] String, arising from a use of `op' at fd.hs:14:38-51
C Bool Bool Bool, arising from a use of `op' at fd.hs:14:20-31
When generalising the type(s) for `bar'
On the other hand, this is fine, but only with a type signature:
baz :: a - a
baz = op True
I don't think this is an intended feature of functional dependencies.
--
Dave Menendez d...@zednenem.com
http://www.eyrie.org/~zednenem/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On Saturday 03 July 2010 2:11:37 pm David Menendez wrote:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
class C a b c | a - b, a - c where
op :: a - b - c
instance C Bool a a where op _ = id
main = putStrLn $ op True done
In this case, I've (arbitrarily) chosen the Bool instance to be a no-op
and pass through the types. Because the dependent types are part of the
declaration header I can use type variables for them.
That's really weird. In particular, I can add this line to your code
without problems:
foo = putStrLn $ if op True True then done else .
but GHC complains about this one:
bar = putStrLn $ if op True True then op True done else .
fd.hs:14:0:
Couldn't match expected type `Bool' against inferred type `[Char]'
When using functional dependencies to combine
C Bool [Char] String, arising from a use of `op' at fd.hs:14:38-51
C Bool Bool Bool, arising from a use of `op' at fd.hs:14:20-31
When generalising the type(s) for `bar'
On the other hand, this is fine, but only with a type signature:
baz :: a - a
baz = op True
I don't think this is an intended feature of functional dependencies.
Indeed. That instance declaration doesn't really make sense, and should
probably be rejected. The functional dependencies on C say that b and c are
dependent on a, so for any particular a, there should be exactly one b and one
c such that C a b c is an instance.
Then the instance declares infinitely many instances C Bool a a. This is a
violation of the fundep. Based on your error message, it looks like it ends up
treating the instance as the first concrete 'a' it comes across, but who
knows?
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On Sat, 03 Jul 2010 12:48:56 -0700, Dan Doel dan.d...@gmail.com wrote: Then the instance declares infinitely many instances C Bool a a. This is a violation of the fundep. Based on your error message, it looks like it ends up treating the instance as the first concrete 'a' it comes across, but who knows? Hmmm.. it doesn't look like a first concrete lockdown. The following works fine: opres1 :: Int - Int opres1 = op True opres2 :: String - String opres2 = op True main = do putStrLn $ op True start putStrLn $ show $ opres1 5 putStrLn $ opres2 $ opres2 $ show $ opres1 6 putStrLn $ opres2 done As a side note, although I agree it abuses the fundeps intent, it was handy for the specific purpose I was implementing to have a no-op/passthrough instance of op. In general I like the typedef approach better, but it looks like I must sacrifice the no-op to make that switch. -- -KQ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On Saturday 03 July 2010 4:01:12 pm Kevin Quick wrote: As a side note, although I agree it abuses the fundeps intent, it was handy for the specific purpose I was implementing to have a no-op/passthrough instance of op. In general I like the typedef approach better, but it looks like I must sacrifice the no-op to make that switch. It's potentially not just a violation of intent, but of soundness. The following code doesn't actually work, but one could imagine it working: class C a b | a - b instance C () a -- Theoretically works because C a b, C a c implies that b ~ c -- -- GHC says b doesn't match c, though. f :: (C a b, C a c) = a - (b - r) - c - r f x g y = g y -- Theoretically valid because both C () a and C () b instances are declared coerce :: forall a b. a - b coerce x = f () (id :: b - b) x -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On Sat, 03 Jul 2010 13:28:44 -0700, Dan Doel dan.d...@gmail.com wrote: As a side note, although I agree it abuses the fundeps intent, it was handy for the specific purpose I was implementing to have a no-op/passthrough instance of op. In general I like the typedef approach better, but it ^^^ should have been type family, not typedef looks like I must sacrifice the no-op to make that switch. It's potentially not just a violation of intent, but of soundness. I agree when examining this from the perspective of the compiler. It's an interesting little wormhole in the safety net usually provided by Haskell (or more properly GHC in this case) to stop people like me from doing foolish things. From the domain of the original problem, having a no-op instance is still desireable, and I achieved this by making the noop instance type polymorphic and use the target concrete type to guide the resolution of the interior family types. class C a where type A2 a type A3 a op :: a - A2 a - A3 a data NoOp x = NoOp instance C (NoOp b) where type A2 (NoOp x) = x type A3 (NoOp x) = x op _ = id This is straightforward and less ambiguous and should therefore be safer as well. Thanks and regards, -- -KQ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] checking types with type families
| Here's a concrete case I recently ran into: | | type family SomeOtherTypeFamily a | class SomeClass a where type SomeType a | instance a ~ SomeOtherTypeFamily b = SomeClass a where |type SomeType a = (b,Int) |-- (error) Not in scope: type variable `b' | | The same thing with fundeps: | | class SomeClass a b | a - b | instance a ~ SomeOtherTypeFamily b = SomeClass a (b,Int) | -- works fine It's not the same thing at all! The code you give certainly should fail. Suppose you use fundeps thus: class C a b | a-b where op :: a - b - b The idiomatic way to replace this with type functions is to remove the 'b' parameter, thus: class C a where type B a op :: a - B a - B a Sometimes you don't want to do this. For example, you might have a bidirectional fundep. Then you can (or rather will be able to) use a superclass thus: class (B a ~ b) = C a b where type B a The superclass says that you can only instantiate this class with a second argument b that is equal to (B a). Thus you might have an instance instance C Int Bool where type B Int = Bool Meanwhile we are working hard on the new type inference engine, which will allow superclass equalities like these. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] checking types with type families
Claus | I'm interested in situations where you think fundeps work | and type families don't. Reason: no one knows how to make | fundeps work cleanly with local type constraints (such as GADTs). | | If you think you have such as case, do send me a test case. | | Do you have a wiki page somewhere collecting these examples? I don't think so. Would you feel like starting one? I do try to turn every tricky example into a case in the testsuite though. | Also, what is the difference between fundeps and type families | wrt local type constraints? I had always assumed them to be | equivalent, if fully implemented. Similar to logic vs functional | programming, where Haskellers tend to find the latter more | convenient. Functional logic programming shows that there | are some tricks missing if one just drops the logic part. Until now, no one has know how to combine fundeps and local constraints. For example class C a b | a-b where op :: a - b instance C Int Bool where op n = n0 data T a where T1 :: T a T2 :: T Int -- Does this typecheck? f :: C a b = T a - Bool f T1 = True f T2 = op 3 The function f should typecheck because inside the T2 branch we know that (a~Int), and hence by the fundep (b~Bool). But we have no formal type system for fundeps that describes this, and GHC's implementation certainly rejects it. In GHC, as in Mark Jones's original descrption, fundeps just give rise to some extra unifications of otherwise under-constrained type variables. Now, Dimitrios and I have recently found that our OutsideIn type system and inference algorithm (described in the Epic Paper on my home page) can easily handle functional dependencies too, by adding a couple of extra rules. That's good news both because it improves our understanding (well, mine anyway); and because it will give GHC a solid implementation, and one that will make the above program typecheck. We are deep in the midst of implementing OutsideIn right now. That said, I'd much prefer to express the program like this: class D a where type B a dop :: a - B a instance D Int where type B Int = Bool dop n = n0 g :: D a = T a - Bool g T1 = True g T2 = dop 3 More perspicuous types, simpler reasoning. Bottom line: I now have a clear idea of how to formalise and implement fundeps; but I am dubious about the long-term software engineering merits of supporting both fundeps and type families. They cover the same territory. Copying Oleg in case he has other counter-examples. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] checking types with type families
| Well, from looking at the documentation, it looks like I could maybe | use a type family if I could write: | | class (DerivedOf a ~ derived) = Typecheck a derived where | ... That's the right idiom yes. But see my message of a few minutes ago... It's neater still to remove the 'derived' parameter altogether, which you can do with uni-directional fundeps. Thus instead of class Typecheck a derived where op :: a - derived you have class Typecheck a where type Derived a op :: a - Derived a | Presumably then I could combine functions 'Typecheck a derived' | constraints without getting lots of Could not deduce (Typecheck a | derived3) from the context (Typecheck a derived13) errors. I'm only | guessing though, because it looks like it's not implemented yet as of | 6.12.3. Correct. These equality superclasses will work in 6.14 and (in a few weeks) in the HEAD, but not in 6.12. But you may not need them if you have unidirectional fundeps. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On Thu, Jul 1, 2010 at 7:54 PM, Simon Peyton-Jones simo...@microsoft.comwrote: | Also, what is the difference between fundeps and type families | wrt local type constraints? I had always assumed them to be | equivalent, if fully implemented. Similar to logic vs functional | programming, where Haskellers tend to find the latter more | convenient. Functional logic programming shows that there | are some tricks missing if one just drops the logic part. Until now, no one has know how to combine fundeps and local constraints. For example class C a b | a-b where op :: a - b instance C Int Bool where op n = n0 data T a where T1 :: T a T2 :: T Int -- Does this typecheck? f :: C a b = T a - Bool f T1 = True f T2 = op 3 The function f should typecheck because inside the T2 branch we know that (a~Int), and hence by the fundep (b~Bool). But we have no formal type system for fundeps that describes this, and GHC's implementation certainly rejects it. Martin Sulzmann, Jeremy Waznyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wazny:Jeremy.html, Peter J. Stuckeyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Stuckey:Peter_J=.html: A Framework for Extended Algebraic Data Types. FLOPS 2006http://www.informatik.uni-trier.de/%7Eley/db/conf/flops/flops2006.html#SulzmannWS06: 47-64 describes such a system, fully implemented in Chameleon, but this system is no longer maintained. Type families and Fundeps are equivalent in expressive power and it's not too hard to show how to encode one in terms of the other. Local constraints are an orthogonal extension. In terms of type inference, type families + local constraints and fundeps + local constraints pose the same challenges. Probably, Simon is refrerring to the 'unresolved' issue of providing a System F style translation for fundeps + local constraints. Well, the point is that System FC is geared toward type families. The two possible solutions are (a) either consider fundeps as syntactic sugar for type families (doesn't quite work once you throw in overlapping instances), (b) design a variant System FC_fundep which has built-in support for fundeps. -Martin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] checking types with type families
Simon Peyton-Jones wrote: I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs). If you think you have such as case, do send me a test case. As an example, is it possible to implement something like: http://okmij.org/ftp/Haskell/deepest-functor.lhs with TF only? I believe the following wiki-page http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap also points out that However, there's a problem: overlap is not allowed at all for type families!! (c) or is it just a question of implementing closed type families? -- View this message in context: http://old.nabble.com/checking-types-with-type-families-tp28967503p29049813.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
I think your problem here is that there's no mention of `a' on the left-hand size of from_val's type signature; you either need to use MPTC+fundep to associate what result is compared to a, or else use a phantom type parameter of Val to make it data Val result a = ... and then from_val :: Val result a - Maybe a. Aha! Why didn't I think of plain old MPTC+fundep? For some reason type families feel a lot more fun. Turns out you can write 'instance Typecheck (SomeMonad result) result' and instead of complaining about a duplicate symbol it unifies 'result', exactly like I wanted. It appears to work like a charm, thanks so much! Though it says it fails the Coverage Condition and I need UndecidableInstances... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] checking types with type families
| I think your problem here is that there's no mention of `a' on the | left-hand size of from_val's type signature; you either need to use | MPTC+fundep to associate what result is compared to a, or else use a | phantom type parameter of Val to make it data Val result a = ... and | then from_val :: Val result a - Maybe a. | | Aha! Why didn't I think of plain old MPTC+fundep? For some reason | type families feel a lot more fun. Turns out you can write 'instance | Typecheck (SomeMonad result) result' and instead of complaining about | a duplicate symbol it unifies 'result', exactly like I wanted. I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs). If you think you have such as case, do send me a test case. Thanks Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs). If you think you have such as case, do send me a test case. Well, from looking at the documentation, it looks like I could maybe use a type family if I could write: class (DerivedOf a ~ derived) = Typecheck a derived where ... Presumably then I could combine functions 'Typecheck a derived' constraints without getting lots of Could not deduce (Typecheck a derived3) from the context (Typecheck a derived13) errors. I'm only guessing though, because it looks like it's not implemented yet as of 6.12.3. So is your question whether I have a use case for fundeps supposing equality constraints in superclass contexts were implemented and they do what I hope they do, or is it do I have a use for those equality constraints as a motivation to implement them? In either case, I can give you some code that works with mptc+fundep but not with type families, unless I'm not using type families correctly of course. But if the type equality thing is coming regardless, then I can just wait for 6.14 or whatever and switch over then. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs). If you think you have such as case, do send me a test case. Do you have a wiki page somewhere collecting these examples? I seem to recall that similar discussions have arisen before and test cases have been provided but I wouldn't know where to check for the currently recorded state of differences. Also, what is the difference between fundeps and type families wrt local type constraints? I had always assumed them to be equivalent, if fully implemented. Similar to logic vs functional programming, where Haskellers tend to find the latter more convenient. Functional logic programming shows that there are some tricks missing if one just drops the logic part. Claus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On 23 June 2010 13:46, Evan Laforge qdun...@gmail.com wrote: I have a parameterized data type: data Val result = VNum Double | VThunk (SomeMonad result) type Environ result = Map Symbol (Val result) I have a class to make it easier to typecheck Vals: class Typecheck a where from_val :: Val result - Maybe a I think your problem here is that there's no mention of `a' on the left-hand size of from_val's type signature; you either need to use MPTC+fundep to associate what result is compared to a, or else use a phantom type parameter of Val to make it data Val result a = ... and then from_val :: Val result a - Maybe a. SPJ's paper on type families has this situation arising in the section on defining a graph class. -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] checking types with type families
On Wednesday 23 June 2010 05:46:46, Evan Laforge wrote: I have a parameterized data type: data Val result = VNum Double | VThunk (SomeMonad result) type Environ result = Map Symbol (Val result) I have a class to make it easier to typecheck Vals: class Typecheck a where from_val :: Val result - Maybe a Would it work if you made Typecheck a two-parameter type class? class Typecheck result a where from_val :: Val result - Maybe a instance Typecheck result Double where ... instance Typecheck result (SomeMonad result) where instance Typecheck Double where from_val (VNum d) = Just d from_val _ = Nothing Now I can write lookup_environ :: (Typecheck a) = Symbol - Environ result - Maybe a Now of course there's a question of how to write Typecheck for VThunk. I would like to be able to call 'lookup_environ' expecting a 'SomeMonad result' and get Nothing or Just depending on if it's present. instance Typecheck (SomeMonad result) where from_val (VThunk f) = Just f But I need something to say that the 'result' from the instance head is the same as the 'result' from the class declaration, because otherwise I get Couldn't match expected type `result' against inferred type `result1' ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
