[Haskell-cafe] Kind-agnostic type classes

[Florian Weimer]

I'm trying to encode a well-known, informally-specified type system in
Haskell.  What causes problems for me is that type classes force types
to be of a specific kind.  The system I'm targeting however assumes that
its equivalent of type classes are kind-agnositic.

For instance, I've got

class Assignable a where
assign :: a -> a -> IO ()

class Swappable a where
swap :: a -> a -> IO ()

class CopyConstructible a where
copy :: a -> IO a

class (Assignable a, CopyConstructible a) => ContainerType a

class (Swappable c, Assignable c, CopyConstructible c) => Container c where
size :: (Num i, ContainerType t) => c t -> IO i

I suppose I could address this with creating aliases for the relevant
classes, but I wonder if there is a better workaround.

I see that the ML module system has a similar restriction on type
sharing.  Is there a fundamental reasons behind this?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Kind-agnostic type classes

[Derek Elkins]

On Fri, 2008-10-03 at 12:22 +0200, Florian Weimer wrote:
> I'm trying to encode a well-known, informally-specified type system in
> Haskell.  What causes problems for me is that type classes force types
> to be of a specific kind.  The system I'm targeting however assumes that
> its equivalent of type classes are kind-agnositic.
> 
> For instance, I've got
> 
> class Assignable a where
> assign :: a -> a -> IO ()
> 
> class Swappable a where
> swap :: a -> a -> IO ()
> 
> class CopyConstructible a where
> copy :: a -> IO a
> 
> class (Assignable a, CopyConstructible a) => ContainerType a
> 
> class (Swappable c, Assignable c, CopyConstructible c) => Container c where
> size :: (Num i, ContainerType t) => c t -> IO i

instane Container Maybe where...

What does copy :: Maybe -> IO Maybe mean?

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Kind-agnostic type classes

[Luke Palmer]

On Fri, Oct 3, 2008 at 4:22 AM, Florian Weimer <[EMAIL PROTECTED]> wrote:
> I'm trying to encode a well-known, informally-specified type system in
> Haskell.  What causes problems for me is that type classes force types
> to be of a specific kind.  The system I'm targeting however assumes that
> its equivalent of type classes are kind-agnositic.

There is no choice of kinds, they are forced by the methods (since the
kind of an actual argument is * by definition).  But see below.

> For instance, I've got
>
> class Assignable a where
>assign :: a -> a -> IO ()
>
> class Swappable a where
>swap :: a -> a -> IO ()
>
> class CopyConstructible a where
>copy :: a -> IO a
>
> class (Assignable a, CopyConstructible a) => ContainerType a
>
> class (Swappable c, Assignable c, CopyConstructible c) => Container c where
>size :: (Num i, ContainerType t) => c t -> IO i

Which is illegal because the three above classes force c to be kind *,
but you're using it here as kind * -> *.

What you want is not this informal "kind-agnostic" classes so much as
quantification in constraints, I presume.  This, if it were supported,
would solve your problem.

class (forall t. Swappable (c t), forall t. Assignable (c t), forall
t. CopyConstructible (c t)) => Contanter c where ...

Incidentally, you *can* do this if you go to a dictionary passing
style (because then you are providing the proofs, rather than asking
the compiler to infer them, which is probably undecidable (what isn't
;-)).

data Assignable a = Assignable { assign :: a -> a -> IO () }
data Swappable a = Swappable { swap :: a -> a -> IO () }
data CopyConstructible a = CopyConstructible { copy :: a -> IO a }
data ContainerType a = ContainerType (Assignable a) (CopyConstructor a)
data Container c t = Container {
   containerAssignable :: forall t. ContainerType t -> Assignable (c t),
   containerSwappable :: forall t. ContainerType t -> Swappable (c t),
   containerCopyConstructible :: forall t. ContainerType t ->
CopyConstructible (c t),
   size :: forall i. (Num i) => ContainerType t -> c t -> IO i }

And then to make an "instance" of Container (construct an object of
it), you need to provide a "proof" of eg. forall t. ContainerType t ->
Assignable (c t).

For what it's worth, this is a well-known but very infrequently used
technique.  Try to come up with something simpler that accomplishes
the "big picture" you have in mind   (spend more time thinking about
the problem and less about the solution you think you want).

Also, OO-esque modeling like this in Haskell almost always leads to
overcomplexity, pain, and desire for yet more "missing" features.  A
more functional solution will serve you well (it takes time to learn
how to come up with functional solutions).

Luke
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Kind-agnostic type classes

[Florian Weimer]

* Derek Elkins:

> On Fri, 2008-10-03 at 12:22 +0200, Florian Weimer wrote:
>> I'm trying to encode a well-known, informally-specified type system in
>> Haskell.  What causes problems for me is that type classes force types
>> to be of a specific kind.  The system I'm targeting however assumes that
>> its equivalent of type classes are kind-agnositic.
>> 
>> For instance, I've got
>> 
>> class Assignable a where
>> assign :: a -> a -> IO ()
>> 
>> class Swappable a where
>> swap :: a -> a -> IO ()
>> 
>> class CopyConstructible a where
>> copy :: a -> IO a
>> 
>> class (Assignable a, CopyConstructible a) => ContainerType a
>> 
>> class (Swappable c, Assignable c, CopyConstructible c) => Container c where
>> size :: (Num i, ContainerType t) => c t -> IO i
>
> instane Container Maybe where...
>
> What does copy :: Maybe -> IO Maybe mean?

Maybe is not an instance of CopyConstructible, so this shouldn't
compile.  On the other hand, for IORef a,

  copy = (>>= newIORef) . readIORef

and for mutable arrays,

  copy = mapArray id

(if I'm not mistaken).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Kind-agnostic type classes

[Florian Weimer]

* Luke Palmer:

>> For instance, I've got
>>
>> class Assignable a where
>>assign :: a -> a -> IO ()
>>
>> class Swappable a where
>>swap :: a -> a -> IO ()
>>
>> class CopyConstructible a where
>>copy :: a -> IO a
>>
>> class (Assignable a, CopyConstructible a) => ContainerType a
>>
>> class (Swappable c, Assignable c, CopyConstructible c) => Container c where
>>size :: (Num i, ContainerType t) => c t -> IO i
>
> Which is illegal because the three above classes force c to be kind *,
> but you're using it here as kind * -> *.
>
> What you want is not this informal "kind-agnostic" classes so much as
> quantification in constraints, I presume.  This, if it were supported,
> would solve your problem.
>
> class (forall t. Swappable (c t), forall t. Assignable (c t), forall
> t. CopyConstructible (c t)) => Contanter c where ...

In the meantime, I figured out that in ML, it suffices to make the
Container type c non-polymorphic (although the syntactic overhead is
rather problematic).  Trying to the same in Haskell, I learnt something
about functional dependencies.  I actually ended up with:

class (Assignable c, CopyConstructible c, Swappable c, ContainerType t, Num s)
=> Container c s t | c -> s, c -> t where
size :: c -> IO Int
empty ::c -> IO Bool

empty c = do
  sz <- size c
  return (sz == 0)

(In fact, I stumbled across "A Comparative Study of Language Support for
Generic Programming" by Garcia et al., which contains a very helpful
Haskell example with functional dependencies and multi-parameter type
classes.)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Kind-agnostic type classes

[David Menendez]

On Fri, Oct 3, 2008 at 9:49 AM, Luke Palmer <[EMAIL PROTECTED]> wrote:
> On Fri, Oct 3, 2008 at 4:22 AM, Florian Weimer <[EMAIL PROTECTED]> wrote:
>> I'm trying to encode a well-known, informally-specified type system in
>> Haskell.  What causes problems for me is that type classes force types
>> to be of a specific kind.  The system I'm targeting however assumes that
>> its equivalent of type classes are kind-agnositic.
>
> There is no choice of kinds, they are forced by the methods (since the
> kind of an actual argument is * by definition).  But see below.
>
>> For instance, I've got
>>
>> class Assignable a where
>>assign :: a -> a -> IO ()
>>
>> class Swappable a where
>>swap :: a -> a -> IO ()
>>
>> class CopyConstructible a where
>>copy :: a -> IO a
>>
>> class (Assignable a, CopyConstructible a) => ContainerType a
>>
>> class (Swappable c, Assignable c, CopyConstructible c) => Container c where
>>size :: (Num i, ContainerType t) => c t -> IO i
>
> Which is illegal because the three above classes force c to be kind *,
> but you're using it here as kind * -> *.
>
> What you want is not this informal "kind-agnostic" classes so much as
> quantification in constraints, I presume.  This, if it were supported,
> would solve your problem.
>
> class (forall t. Swappable (c t), forall t. Assignable (c t), forall
> t. CopyConstructible (c t)) => Contanter c where ...
>
> Incidentally, you *can* do this if you go to a dictionary passing
> style (because then you are providing the proofs, rather than asking
> the compiler to infer them, which is probably undecidable (what isn't
> ;-)).

You don't necessarily need explicit dictionaries.

For example, I've occasionally wanted to have a constraint (forall a.
Show a => Show (f a)). One fairly simple way to do this to declare a
new class.

class Show1 f where
showsPrec1 :: (Show a) => Int -> f a -> ShowS

instance Show1 [] where
showsPrec1 = showsPrec

The same technique is used in Data.Typeable.

-- 
Dave Menendez <[EMAIL PROTECTED]>

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe