Hi, all! I guess this belongs to haskell-cafe or glasgow-haskell-users, but I've already been there and got no replies. Thanks in advance for anyone taking the time to read on. Given two type classes A t and B t, I'd like the typechecker to derive different A t instances depending exactly on whether t is an instance of B. In other words, is it possible to define a class (actually a type-level function) IsB t f such that: IsB t HTrue <=> instance (B t) exists IsB t HFalse <=> otherwise? If not, is this wish intrisically pointless? After experimenting a bit with multiparameter classes, overlapping instances and suchlike, it looks like Haskell is being purposedly designed not to support this. Yes, I believe that would require the typechecker to take a whole new theorem-proving (undecidable?) stance :o) On the other hand, any interesting type-level programming seems to require undecidable+overlapping instances, so we are usually working on undecidable grounds... Sorry if this is an overdebated matter (is it?), but searching through the endless haskell archives is not trivial. Thanks in advance for any pointers or thoughts on the matter. Cheers, Jorge. _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
On 1/9/08, Jorge Marques Pelizzoni <[hidden email]> wrote:
> Given two type classes A t and B t, I'd like the typechecker to derive > different A t instances depending exactly on whether t is an instance of > B. I think this would require some kind of whole-program analysis. While Haskell provides assertions that t is an instance of B (B t), it does *not* provide assertions that t is not an instance of B. This is because an instance of B can be declared by other modules at a later point (e.g. by someone who imports your module). -- Taral <[hidden email]> "Please let me know if there's any further trouble I can give you." -- Unknown _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
In reply to this post by Jorge Marques Pelizzoni
> Given two type classes A t and B t, I'd like the typechecker to derive
> different A t instances depending exactly on whether t is an instance of > B. In other words, is it possible to define a class (actually a type-level > function) IsB t f such that: A GHC-like type system is in principle powerful enough to do just that. We exploit such capability in HList and OOHaskell. That is, the class whose instance availability should be observed must be first set up to carry an extra functionally dependent type parameter that specifically is meant to report back on instance availability. Then, we sacrifice the capability of a generic default instance for that class to indeed report back the lack of an instance through a type-level False on the new type-parameter position, whereas all normal instances report back type-level True. The usual problem of functional-dependency violation occurs, that is, the generic default instance is not entirely standard because if it says to return False for all types, then the other instances can't claim the opposite unless we had special fundep rules for generic default instances. However, we can recover from that by making the generic default instance vacuously generic in the type-level Boolean result position so that it becomes strictly more general than any specific instance, while we still assign type-level False to the position but by a type-level cast (instead of a verbatim False). Type-level type cast is the type-level programmer's swiss army knife. See the illustration below. HTH, Ralf {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-overlapping-instances #-} {-# OPTIONS -fallow-undecidable-instances #-} module M2 where import M1 instance TypeCast x x where typeCast = id main = do print $ b $ hasInstance ST1 print $ b $ hasInstance ST2 {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-overlapping-instances #-} {-# OPTIONS -fallow-undecidable-instances #-} module M1 where -- Type-level Booleans data T -- True data F -- False class B x where b :: x -> Bool instance B T where b = const True instance B F where b = const False -- Sample types data ST1 = ST1 data ST2 = ST2 -- A class that reports on instance availability class B b => R x b | x -> b instance R ST1 T instance (B b, TypeCast F b) => R x b -- generically missing instance -- Observe instance availability hasInstance :: R x b => x -> b hasInstance _ = undefined -- The key weapon class TypeCast x y | x -> y, y -> x where typeCast :: x -> y _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
Thank you very much, Ralf, for your very thorough reply. That's a very general way to deal with the issue. It never occurred to me that the "inspected" class itself might carry the availability info. Cheers, Jorge. Ralf Laemmel escreveu: >> Given two type classes A t and B t, I'd like the typechecker to derive >> different A t instances depending exactly on whether t is an instance of >> B. In other words, is it possible to define a class (actually a >> type-level >> function) IsB t f such that: > > A GHC-like type system is in principle powerful enough to do just > that. We exploit such capability in HList and OOHaskell. That is, the > class whose instance availability should be observed must be first set > up to carry an extra functionally dependent type parameter that > specifically is meant to report back on instance availability. Then, > we sacrifice the capability of a generic default instance for that > class to indeed report back the lack of an instance through a > type-level False on the new type-parameter position, whereas all > normal instances report back type-level True. The usual problem of > functional-dependency violation occurs, that is, the generic default > instance is not entirely standard because if it says to return False > for all types, then the other instances can't claim the opposite > unless we had special fundep rules for generic default instances. > However, we can recover from that by making the generic default > instance vacuously generic in the type-level Boolean result position > so that it becomes strictly more general than any specific instance, > while we still assign type-level False to the position but by a > type-level cast (instead of a verbatim False). > > Type-level type cast is the type-level programmer's swiss army knife. > > See the illustration below. > > HTH, > Ralf > > > {-# OPTIONS -fglasgow-exts #-} > {-# OPTIONS -fallow-overlapping-instances #-} > {-# OPTIONS -fallow-undecidable-instances #-} > > module M2 where > > import M1 > > instance TypeCast x x where typeCast = id > > main = > do > print $ b $ hasInstance ST1 > print $ b $ hasInstance ST2 > > > {-# OPTIONS -fglasgow-exts #-} > {-# OPTIONS -fallow-overlapping-instances #-} > {-# OPTIONS -fallow-undecidable-instances #-} > > module M1 where > > -- Type-level Booleans > data T -- True > data F -- False > class B x where b :: x -> Bool > instance B T where b = const True > instance B F where b = const False > > -- Sample types > data ST1 = ST1 > data ST2 = ST2 > > -- A class that reports on instance availability > class B b => R x b | x -> b > instance R ST1 T > instance (B b, TypeCast F b) => R x b -- generically missing instance > > -- Observe instance availability > hasInstance :: R x b => x -> b > hasInstance _ = undefined > > -- The key weapon > class TypeCast x y | x -> y, y -> x > where > typeCast :: x -> y > Jorge M. Pelizzoni ICMC - Universidade de São Paulo _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
In reply to this post by Ralf Laemmel
On Jan 9, 2008 3:10 PM, Ralf Laemmel <[hidden email]> wrote: Type-level type cast is the type-level programmer's swiss army knife.
Does this get any easier with type families? Your (TypeCast a b) seems similar in intent to (a ~ b), but I'm not familiar enough with the latter to know whether it would work here.
-- Dave Menendez <[hidden email]> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
Free forum by Nabble | Edit this page |