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)
2013-09-15 11:16, oleg@okmij.org 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
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.
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,
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.
participants (3)
-
Emil Axelsson -
Evan Laforge -
oleg＠okmij.org