Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion
Ryan Newton wrote: 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. Your code essentially accomplishes the goal: data E m where Assign :: AssignCap m = V - E m - E m - E m Varref :: V - E m -- ... Every time you construct the value of the type (E m) with the Assign constructor, you have to constructively prove -- provide evidence for -- that the type m is a member of AssignCap. That evidence is stored within the E m value and so can be reused whenever it is needed later. Let us modify the example slightly: class AssignCap m class MutateCap m data E m where Assign :: AssignCap m = V - E m - E m - E m Mutate :: MutateCap m = V - E m - E m - E m Varref :: V - E m -- ... type V = String -- test1 :: E t - E t test1 (Assign v x1 x2) = Assign v x1 x2 -- test2 :: MutateCap t = E t - E t test2 (Assign v x1 x2) = Mutate v x1 x2 To use the constructor Assign, we need the evidence that AssignCap m holds. The deconstructed value (Assign v x1 x2) provides such an evidence (as a `hidden' field of the data type). Therefore, the inferred type for test1 has no constraints. In contrast, in test2 nothing provides Mutate with the evidence that MutateCap m holds. Therefore, the inferred type has the MutateCap m constraint. If storing the evidence is not desired, then one should use ordinary ADT with smart constructors: -- Data constructors should not be exported data E1 m = Assign1 V (E1 m) (E1 m) | Varref1 V isAssign (Assign1 v x1 x2) = Just (v,x1,x2) isAssign _ = Nothing assign :: AssignCap m = V - E1 m - E1 m - E1 m assign = Assign1 -- test3 :: AssignCap m = E1 m - E1 m test3 e | Just (v,x1,x2) - isAssign e = assign v x1 x2 OCaml has a so-called private constructors, which permit deconstruction but prohibit construction. They are quite handy, saving us trouble writing the views like isAssign. 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). The key word in the phrase ``certain cases are forbidden based on the type'' is _type_ -- rather than a type class. If you wish to use this special GADT feature, you have to `invert' your design. Rather than specifying what is _required_ to construct an (E m) value, you should specify what is _provided_. data E2 m where Assign2 :: V - E2 m - E2 m - E2 IOT Varref2 :: V - E2 PureT test4 :: E2 IOT - E2 IOT test4 (Assign2 v x1 x2) = Assign2 v x1 x2 test4 (Varref2 _) = undefined The compiler complaints Couldn't match type `IOT' with `PureT' Inaccessible code in a pattern with constructor Varref2 :: V - E2 PureT, in an equation for `test4' In the pattern: Varref2 _ In an equation for `test4': test4 (Varref2 _) = undefined as desired. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion
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-boun...@haskell.org
[mailto:haskell-cafe-boun...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion
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
dimit...@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-boun...@haskell.org [mailto:
haskell-cafe-boun...@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
** **
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
