[Haskell] detecting existing instances

[Ralf Laemmel]

> 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