detecting existing instances

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

detecting existing instances

Jorge Marques Pelizzoni

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
Reply | Threaded
Open this post in threaded view
|

Re: detecting existing instances

Taral
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
Reply | Threaded
Open this post in threaded view
|

Re: detecting existing instances

Ralf Laemmel
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
Reply | Threaded
Open this post in threaded view
|

Re: 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

_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: detecting existing instances

David Menendez-2
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. 

See the illustration below.

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