[Haskell] detecting existing instances

[Jorge Marques Pelizzoni]

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