Re: reifying typeclasses

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

Re: reifying typeclasses

oleg-30

Evan Laforge wrote:

> I have a typeclass which is instantiated across a closed set of 3
> types.  It has an ad-hoc set of methods, and I'm not too happy with
> them because being a typeclass forces them to all be defined in one
> place, breaking modularity.  A sum type, of course, wouldn't have that
> problem.  But in other places I want the type-safety that separate
> types provide, and packing everything into a sum type would destroy
> that.  So, expression problem-like, I guess.
>
> It seems to me like I should be able to replace a typeclass with
> arbitrary methods with just two, to reify the type and back.  This
> seems to work when the typeclass dispatches on an argument, but not on
> a return value.  E.g.:


If the universe (the set of types of interest to instantiate the type
class to) is closed, GADTs spring to mind immediately. See, for
example, the enclosed code. It is totally unproblematic (one should
remember to always write type signatures when programming with
GADTs. Weird error messages otherwise ensue.)

One of the most notable differences between GADT and type-class--based
programming is that GADTs are closed and type classes are open (that
is, new instances can be added at will). In fact, a less popular
technique of implementing type classes (which has been used in some Haskell
systems -- but not GHC)) is intensional type analysis, or typecase.
It is quite similar to the GADT solution.


The main drawback of the intensional type analysis as shown in the
enclosed code is that it breaks parametricity. The constraint Eq a
does not let one find out what the type 'a' is and so what other
operations it may support. (Eq a) says that the type a supports (==),
and does not say any more than that. OTH, Representable a tells quite
a lot about type a, essentially, everything.

> types.  It has an ad-hoc set of methods, and I'm not too happy with
> them because being a typeclass forces them to all be defined in one
> place, breaking modularity.  A sum type, of course, wouldn't have that
Why not to introduce several type classes, even a type class for each
method if necessary. Grouping methods under one type class is
appropriate when such a grouping makes sense. Otherwise, Haskell won't
lose in expressiveness if a type class could have only one method.

{-# LANGUAGE GADTs #-}

module G where

data TRep a where
    TInt  :: TRep Int
    TChar :: TRep Char

class Representable a where
    repr :: TRep a

instance Representable Int where
    repr = TInt

instance Representable Char where
    repr = TChar

argument :: Representable a => a -> Int
argument x = go repr x
 where
 -- For GADTs, signatures are important!
 go :: TRep a -> a -> Int
 go TInt  x = x
 go TChar x = fromEnum x

-- just the `mirror inverse'
result :: Representable a => Int -> a
result x = go repr x
 where
 -- For GADTs, signatures are important!
 go :: TRep a -> Int -> a
 go TInt  x = x
 go TChar x = toEnum x

t1 = argument 'a'
t2 = show (result 98 :: Char)

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

Re: reifying typeclasses

oleg-30

[I too had the problem sending this e-mail to Haskell list.
I got a reply saying the message awaits moderator approval]

Evan Laforge wrote:

> I have a typeclass which is instantiated across a closed set of 3
> types.  It has an ad-hoc set of methods, and I'm not too happy with
> them because being a typeclass forces them to all be defined in one
> place, breaking modularity.  A sum type, of course, wouldn't have that
> problem.  But in other places I want the type-safety that separate
> types provide, and packing everything into a sum type would destroy
> that.  So, expression problem-like, I guess.
>
> It seems to me like I should be able to replace a typeclass with
> arbitrary methods with just two, to reify the type and back.  This
> seems to work when the typeclass dispatches on an argument, but not on
> a return value.  E.g.:


If the universe (the set of types of interest to instantiate the type
class to) is closed, GADTs spring to mind immediately. See, for
example, the enclosed code. It is totally unproblematic (one should
remember to always write type signatures when programming with
GADTs. Weird error messages otherwise ensue.)

One of the most notable differences between GADT and type-class--based
programming is that GADTs are closed and type classes are open (that
is, new instances can be added at will). In fact, a less popular
technique of implementing type classes (which has been used in some Haskell
systems -- but not GHC)) is intensional type analysis, or typecase.
It is quite similar to the GADT solution.


The main drawback of the intensional type analysis as shown in the
enclosed code is that it breaks parametricity. The constraint Eq a
does not let one find out what the type 'a' is and so what other
operations it may support. (Eq a) says that the type a supports (==),
and does not say any more than that. OTH, Representable a tells quite
a lot about type a, essentially, everything.

> types.  It has an ad-hoc set of methods, and I'm not too happy with
> them because being a typeclass forces them to all be defined in one
> place, breaking modularity.  A sum type, of course, wouldn't have that
Why not to introduce several type classes, even a type class for each
method if necessary. Grouping methods under one type class is
appropriate when such a grouping makes sense. Otherwise, Haskell won't
lose in expressiveness if a type class could have only one method.

{-# LANGUAGE GADTs #-}

module G where

data TRep a where
    TInt  :: TRep Int
    TChar :: TRep Char

class Representable a where
    repr :: TRep a

instance Representable Int where
    repr = TInt

instance Representable Char where
    repr = TChar

argument :: Representable a => a -> Int
argument x = go repr x
 where
 -- For GADTs, signatures are important!
 go :: TRep a -> a -> Int
 go TInt  x = x
 go TChar x = fromEnum x

-- just the `mirror inverse'
result :: Representable a => Int -> a
result x = go repr x
 where
 -- For GADTs, signatures are important!
 go :: TRep a -> Int -> a
 go TInt  x = x
 go TChar x = toEnum x

t1 = argument 'a'
t2 = show (result 98 :: Char)

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

Re: reifying typeclasses

Emil Axelsson-2
In reply to this post by oleg-30
2013-09-15 11:16, [hidden email] skrev:

> Evan Laforge wrote:
>> I have a typeclass which is instantiated across a closed set of 3
>> types.  It has an ad-hoc set of methods, and I'm not too happy with
>> them because being a typeclass forces them to all be defined in one
>> place, breaking modularity.  A sum type, of course, wouldn't have that
>> problem.  But in other places I want the type-safety that separate
>> types provide, and packing everything into a sum type would destroy
>> that.  So, expression problem-like, I guess.
>>
>> It seems to me like I should be able to replace a typeclass with
>> arbitrary methods with just two, to reify the type and back.  This
>> seems to work when the typeclass dispatches on an argument, but not on
>> a return value.  E.g.:
>
> If the universe (the set of types of interest to instantiate the type
> class to) is closed, GADTs spring to mind immediately. See, for
> example, the enclosed code. It is totally unproblematic (one should
> remember to always write type signatures when programming with
> GADTs. Weird error messages otherwise ensue.)
>
> One of the most notable differences between GADT and type-class--based
> programming is that GADTs are closed and type classes are open (that
> is, new instances can be added at will). In fact, a less popular
> technique of implementing type classes (which has been used in some Haskell
> systems -- but not GHC)) is intensional type analysis, or typecase.
> It is quite similar to the GADT solution.

I've been toying with using Data Types à la Carte to get type
representations, a `Typeable` class and dynamic types parameterized by a
possibly open universe:

   https://github.com/emilaxelsson/dsl-factory/blob/master/TypeReify.hs

Using this module (which depends on the syntactic package), Evan's
problem can be solved easily without setting up any new classes or data
types, as shown below.

/ Emil



import Language.Syntactic
import TypeReify

type Universe = IntType :+: CharType

argument :: forall a . Typeable Universe a => a -> Int
argument a
     | Just IntType  <- prj t = a
     | Just CharType <- prj t = fromEnum a
         -- Note: All cases are covered, since `Universe` is closed
   where
     TypeRep t = typeRep :: TypeRep Universe a

result :: forall a . Typeable Universe a => Int -> a
result a
     | Just IntType  <- prj t = a
     | Just CharType <- prj t = toEnum a
         -- Note: All cases are covered, since `Universe` is closed
   where
     TypeRep t = typeRep :: TypeRep Universe a

-- Note that we do not have to use a closed universe. Here's an alternative,
-- open version of `argument`:
argument' :: forall u a . (IntType :<: u, CharType :<: u) =>
              Typeable u a => a -> Int
argument' a
     | Just IntType  <- prj t = a
     | Just CharType <- prj t = fromEnum a
     | otherwise              = 0  -- or whatever :)
   where
     TypeRep t = typeRep :: TypeRep u a

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

Re: reifying typeclasses

Evan Laforge
In reply to this post by oleg-30
Thanks to everyone who replied, indeed it looks like GADTs do what I
claimed I wanted. That's neat because I've never been able to think of
a use for them.  However:

On Sun, Sep 15, 2013 at 2:16 AM,  <[hidden email]> wrote:
> Why not to introduce several type classes, even a type class for each
> method if necessary. Grouping methods under one type class is
> appropriate when such a grouping makes sense. Otherwise, Haskell won't
> lose in expressiveness if a type class could have only one method.

That's a very good point too, and one I should have thought of first.
 It's the simplest and I think most idiomatic.  Ok, I guess I'm back
to not being able to think of a use for GADTs, it seems like that
happens whenever I think I have a use for a fancy feature :)

> The main drawback of the intensional type analysis as shown in the
> enclosed code is that it breaks parametricity. The constraint Eq a

I guess what you're saying is that since I'm implementing a
typeswitch, then I lose the nice feature of typeclasses that I know it
can't do anything with the value except what the typeclass provides.
In a sense, it loses type safety because it's too generic.  That's a
good point too.  No free lunch, I guess, you get one thing and lose
another.  Typeclasses, though, don't exploit the closed universe part,
though I can't think offhand how that hurts me.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: reifying typeclasses

oleg-30
In reply to this post by Emil Axelsson-2

> I've been toying with using Data Types a la Carte to get type
> representations, a `Typeable` class and dynamic types parameterized by a
> possibly open universe:

If the universe is potentially open, and if we don't care about
exhaustive pattern-matching check (which is one of the principal
benefits of GADTs -- pronounced in dependently-typed languages), the
problem can be solved far more simply. No type classes, no instances,
no a la Carte, to packages other than the base.

{-# LANGUAGE ScopedTypeVariables #-}

module GG where

import Data.Typeable

argument :: Typeable a => a -> Int
argument a
     | Just (x::Int)  <- cast a = x
     | Just (x::Char) <- cast a = fromEnum x

result :: Typeable a => Int -> a
result x
  | Just r  <- cast (id x)              = r
  | Just r  <- cast ((toEnum x)::Char)  = r

t1 = argument 'a'
t2 = show (result 98 :: Char)


That is it, quite symmetrically. This is essentially how type classes
are implemented on some systems (Chameleoon, for sure, and probably
JHC). By this solution we also gave up on parametricity. Which is why
such a solution is probably better kept `under the hood', as an
implementation of type classes.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe