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