[Haskell-cafe] Re: [Haskell] Re: Proposal: unification of style offunction/data/type/class definitions

[Brian Hulley]

Bulat Ziganshin wrote:
> sequence :: [m a] -> m [a] | Monad m

I think translations of higher rank signatures using this syntax could be:

    foo :: (forall a. a-> a) ->b -> c -> (b,c)

==>

    foo :: (a -> a | a) -> b -> c -> (b, c)

using the rule that we just write the variable by itself to indicate the 
quantification point.

With restricted quantification,

    bar :: forall m a b. MonadIO m => (forall n. MonadIO n => a -> n b) -> 
a -> m b

==>

    bar :: (a -> n b | n, MonadIO n) -> a -> m b | a, b, m, MonadIO m

Perhaps some rules could be devised to automatically determine the 
quantification point of each variable so it might even be possible to write 
the above as:

    bar :: (a -> n b | MonadIO n) -> a -> m b | MonadIO m

though for MPTC it's no longer clear from a restriction which variable(s) 
are being introduced and which are being used as the basis for restricting 
them, hence explicit quantification as above is probably unavoidable for the 
general case.

Neil Mitchell wrote:
> How about name, context, value as the three elements:
>
> class <name> | <context> where <value>
> data <name> | <context> = <value>
> type <name> | <context> = <value>
>  <name> | <context> :: <value>

This would give:

    sequence | Monad m :: [m a] -> m [a]

But this wouldn't work because here the context is separated from the rest 
of the type by :: whereas from the higher rank examples above it's clear 
that the context, which is nothing more than a(restricted) quantifier, needs 
to be part of the type itself.

Regards, Brian.
-- 
Logic empowers us and Love gives us purpose.
Yet still phantoms restless for eras long past,
congealed in the present in unthought forms,
strive mightily unseen to destroy us.

http://www.metamilk.com