Type checking oddity -- maybe my own confusion
Hi all, Is there something wrong with the code below? My anticipation was that the type of "test" would include the class constraint, because it uses the Assign constructor. But if you load this code in GHCI you can see that the inferred type was "test :: E m -> E m". Thanks, -Ryan {-# LANGUAGE GADTs #-} class AssignCap m data PureT data IOT instance AssignCap IOT data E m where Assign :: AssignCap m => V -> E m -> E m -> E m Varref :: V -> E m -- ... type V = String -- I expected the following type but am not getting it: -- test :: AssignCap m => E m -> E m test x = case x of Assign v e1 e2 -> Assign v e1 e2 -- And this is the same: Assign v e1 e2 -> x
Hi Ryan, Think of AssignCap as an extra argument packaged up with the Assign constructor. When you pattern match against Assign you make the AssignCap constraint *available* for use in the RHS of the pattern; so there's no need for quantification, you already have the constraint you want packaged inside your argument. (Back in the old times when GHC did not implement implication constraints maybe you'd get the type you say). Does that help? Thanks d- From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Ryan Newton Sent: 12 July 2011 16:02 To: Haskell Cafe Subject: [Haskell-cafe] Type checking oddity -- maybe my own confusion Hi all, Is there something wrong with the code below? My anticipation was that the type of "test" would include the class constraint, because it uses the Assign constructor. But if you load this code in GHCI you can see that the inferred type was "test :: E m -> E m". Thanks, -Ryan {-# LANGUAGE GADTs #-} class AssignCap m data PureT data IOT instance AssignCap IOT data E m where Assign :: AssignCap m => V -> E m -> E m -> E m Varref :: V -> E m -- ... type V = String -- I expected the following type but am not getting it: -- test :: AssignCap m => E m -> E m test x = case x of Assign v e1 e2 -> Assign v e1 e2 -- And this is the same: Assign v e1 e2 -> x
Thanks, that does help. Very clear description. Any good ideas about how to tweak my example to do what was intended ;-)? The desired goal was that everywhere I construct a value using the Assign constructor, that the resulting value's type to be tainted by the AssignCap constraint. Actually... to go a bit further, I thought there was some way to arrange this so that, upon GHC type-checking the case statement, it would realize that certain cases are forbidden based on the type, and would consider the pattern match complete without them (or issue an error if they are present). Thanks, -Ryan On Tue, Jul 12, 2011 at 11:17 AM, Dimitrios Vytiniotis < dimitris@microsoft.com> wrote:
Hi Ryan, ****
** **
Think of AssignCap as an extra argument packaged up with the Assign constructor. When ****
you pattern match against Assign you make the AssignCap constraint ** available** for use in****
the RHS of the pattern; so there’s no need for quantification, you already have the constraint****
you want packaged inside your argument. (Back in the old times when GHC did not implement ****
implication constraints maybe you’d get the type you say). Does that help? ****
** **
Thanks****
d-****
** **
** **
*From:* haskell-cafe-bounces@haskell.org [mailto: haskell-cafe-bounces@haskell.org] *On Behalf Of *Ryan Newton *Sent:* 12 July 2011 16:02 *To:* Haskell Cafe *Subject:* [Haskell-cafe] Type checking oddity -- maybe my own confusion** **
** **
Hi all,****
** **
Is there something wrong with the code below? My anticipation was that the type of "test" would include the class constraint, because it uses the Assign constructor. But if you load this code in GHCI you can see that the inferred type was "test :: E m -> E m".****
** **
Thanks,****
-Ryan****
** **
** **
{-# LANGUAGE GADTs #-}****
** **
class AssignCap m ****
data PureT ****
data IOT ****
instance AssignCap IOT ****
** **
data E m where ****
Assign :: AssignCap m => V -> E m -> E m -> E m****
Varref :: V -> E m****
-- ...****
** **
type V = String****
** **
-- I expected the following type but am not getting it:****
-- test :: AssignCap m => E m -> E m****
test x = ****
case x of ****
Assign v e1 e2 -> Assign v e1 e2****
-- And this is the same:****
Assign v e1 e2 -> x****
** **
On 07/12/2011 05:01 PM, Ryan Newton wrote:
Hi all,
Is there something wrong with the code below? My anticipation was that the type of "test" would include the class constraint, because it uses the Assign constructor. But if you load this code in GHCI you can see that the inferred type was "test :: E m -> E m".
When I complete the pattern match in 'test', it might look like this: test x = case x of Assign v e1 e2 -> x Varref v -> x (which is just id :: E m -> E m). Of course, we want to be able to write
test (Varref v)
for any v :: V, and match the second case. But as 'Varref' does not add an AssignCap constraint, 'test' must not either. Hope that helps. Steffen
Thanks, -Ryan
{-# LANGUAGE GADTs #-}
class AssignCap m data PureT data IOT instance AssignCap IOT
data E m where Assign :: AssignCap m => V -> E m -> E m -> E m Varref :: V -> E m -- ...
type V = String
-- I expected the following type but am not getting it: -- test :: AssignCap m => E m -> E m test x = case x of Assign v e1 e2 -> Assign v e1 e2 -- And this is the same: Assign v e1 e2 -> x
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
Dimitrios Vytiniotis -
Ryan Newton -
Steffen Schuldenzucker