Dan Doel | 6 Dec 19:59 2011
Picon

More liberal than liberal type synonyms

Greetings,

In the process of working on a Haskell-alike language recently, Ed
Kmett and I realized that we had (without really thinking about it)
implemented type synonyms that are a bit more liberal than GHC's. With
LiberalTypeSynonyms enabled, GHC allows:

    type Foo a b = b -> a
    type Bar f = f String Int

    baz :: Bar Foo
    baz = show

because Bar expands to saturate Foo. However, we had also implemented
the following, which fails in GHC:

    type Foo a b = b -> a
    type Bar f = f (Foo Int) (Foo Int)
    type Baz f g = f Int -> g Int

    quux :: Bar Baz
    quux = id

That is: type synonyms are allowed to be partially applied within
other type synonyms, as long as similar transitive saturation
guarantees are met during their use.

I don't know how useful it is, but I was curious if anyone can see
anything wrong with allowing this (it seems okay to me after a little
thought), and thought I'd float the idea out to the GHC developers, in
(Continue reading)

Dmitry Kulagin | 7 Dec 11:48 2011
Picon

Re: More liberal than liberal type synonyms

Hi Dan,

I am still pretty new in Haskell, but this problem annoys me already.

If I define certain monad as a type synonym:

    type StateA a = StateT SomeState SomeMonad a

Then I can't declare new monad based on the synonym:

    type StateB a = StateT SomeOtherState StateA a

The only way I know to overcome is to declare StateA without `a':

    type StateA = StateT SomeState SomeMonad

But it is not always possible with existing code base.

I am sorry, if this is offtopic, but it seemed to me that the problem
is realted to partially applied type synomyms you described.

Thanks!
Dmitry

On Tue, Dec 6, 2011 at 10:59 PM, Dan Doel <dan.doel <at> gmail.com> wrote:
> Greetings,
>
> In the process of working on a Haskell-alike language recently, Ed
> Kmett and I realized that we had (without really thinking about it)
> implemented type synonyms that are a bit more liberal than GHC's. With
(Continue reading)

Øystein Kolsrud | 7 Dec 12:09 2011
Picon

Re: More liberal than liberal type synonyms

You should be able to write something like this:

type StateB a b = StateT SomeOtherState (StateA a) b

Best regards, Øystein Kolsrud

On Wed, Dec 7, 2011 at 11:48 AM, Dmitry Kulagin <dmitry.kulagin <at> gmail.com> wrote:
Hi Dan,

I am still pretty new in Haskell, but this problem annoys me already.

If I define certain monad as a type synonym:

   type StateA a = StateT SomeState SomeMonad a

Then I can't declare new monad based on the synonym:

   type StateB a = StateT SomeOtherState StateA a

The only way I know to overcome is to declare StateA without `a':

   type StateA = StateT SomeState SomeMonad

But it is not always possible with existing code base.

I am sorry, if this is offtopic, but it seemed to me that the problem
is realted to partially applied type synomyms you described.

Thanks!
Dmitry

On Tue, Dec 6, 2011 at 10:59 PM, Dan Doel <dan.doel <at> gmail.com> wrote:
> Greetings,
>
> In the process of working on a Haskell-alike language recently, Ed
> Kmett and I realized that we had (without really thinking about it)
> implemented type synonyms that are a bit more liberal than GHC's. With
> LiberalTypeSynonyms enabled, GHC allows:
>
>    type Foo a b = b -> a
>    type Bar f = f String Int
>
>    baz :: Bar Foo
>    baz = show
>
> because Bar expands to saturate Foo. However, we had also implemented
> the following, which fails in GHC:
>
>    type Foo a b = b -> a
>    type Bar f = f (Foo Int) (Foo Int)
>    type Baz f g = f Int -> g Int
>
>    quux :: Bar Baz
>    quux = id
>
> That is: type synonyms are allowed to be partially applied within
> other type synonyms, as long as similar transitive saturation
> guarantees are met during their use.
>
> I don't know how useful it is, but I was curious if anyone can see
> anything wrong with allowing this (it seems okay to me after a little
> thought), and thought I'd float the idea out to the GHC developers, in
> case they're interested in picking it up.
>
> -- Dan
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe



--
Mvh Øystein Kolsrud
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Dmitry Kulagin | 7 Dec 12:20 2011
Picon

Re: More liberal than liberal type synonyms

> You should be able to write something like this:
>
> type StateB a b = StateT SomeOtherState (StateA a) b

Thank you for reply, but this variant actually does not compile:
StateA and (StateA a) have different kinds.

Dmitry

>
> Best regards, Øystein Kolsrud
>
>
> On Wed, Dec 7, 2011 at 11:48 AM, Dmitry Kulagin <dmitry.kulagin <at> gmail.com>
> wrote:
>>
>> Hi Dan,
>>
>> I am still pretty new in Haskell, but this problem annoys me already.
>>
>> If I define certain monad as a type synonym:
>>
>>    type StateA a = StateT SomeState SomeMonad a
>>
>> Then I can't declare new monad based on the synonym:
>>
>>    type StateB a = StateT SomeOtherState StateA a
>>
>> The only way I know to overcome is to declare StateA without `a':
>>
>>    type StateA = StateT SomeState SomeMonad
>>
>> But it is not always possible with existing code base.
>>
>> I am sorry, if this is offtopic, but it seemed to me that the problem
>> is realted to partially applied type synomyms you described.
>>
>> Thanks!
>> Dmitry
>>
>> On Tue, Dec 6, 2011 at 10:59 PM, Dan Doel <dan.doel <at> gmail.com> wrote:
>> > Greetings,
>> >
>> > In the process of working on a Haskell-alike language recently, Ed
>> > Kmett and I realized that we had (without really thinking about it)
>> > implemented type synonyms that are a bit more liberal than GHC's. With
>> > LiberalTypeSynonyms enabled, GHC allows:
>> >
>> >    type Foo a b = b -> a
>> >    type Bar f = f String Int
>> >
>> >    baz :: Bar Foo
>> >    baz = show
>> >
>> > because Bar expands to saturate Foo. However, we had also implemented
>> > the following, which fails in GHC:
>> >
>> >    type Foo a b = b -> a
>> >    type Bar f = f (Foo Int) (Foo Int)
>> >    type Baz f g = f Int -> g Int
>> >
>> >    quux :: Bar Baz
>> >    quux = id
>> >
>> > That is: type synonyms are allowed to be partially applied within
>> > other type synonyms, as long as similar transitive saturation
>> > guarantees are met during their use.
>> >
>> > I don't know how useful it is, but I was curious if anyone can see
>> > anything wrong with allowing this (it seems okay to me after a little
>> > thought), and thought I'd float the idea out to the GHC developers, in
>> > case they're interested in picking it up.
>> >
>> > -- Dan
>> >
>> > _______________________________________________
>> > Haskell-Cafe mailing list
>> > Haskell-Cafe <at> haskell.org
>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe <at> haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
>
>
> --
> Mvh Øystein Kolsrud
Yves Parès | 7 Dec 12:33 2011
Picon

Re: More liberal than liberal type synonyms

This is impossible:
in the definition of 'StateT s m a', m must be a monad and then have the * -> * kind.
So you cannot pass (StateA a), because it has simply the * kind.

Dmitry, does your code work with LiberalTypeSynonyms extention activated?

2011/12/7 Øystein Kolsrud <kolsrud <at> gmail.com>
You should be able to write something like this:

type StateB a b = StateT SomeOtherState (StateA a) b

Best regards, Øystein Kolsrud


On Wed, Dec 7, 2011 at 11:48 AM, Dmitry Kulagin <dmitry.kulagin <at> gmail.com> wrote:
Hi Dan,

I am still pretty new in Haskell, but this problem annoys me already.

If I define certain monad as a type synonym:

   type StateA a = StateT SomeState SomeMonad a

Then I can't declare new monad based on the synonym:

   type StateB a = StateT SomeOtherState StateA a

The only way I know to overcome is to declare StateA without `a':

   type StateA = StateT SomeState SomeMonad

But it is not always possible with existing code base.

I am sorry, if this is offtopic, but it seemed to me that the problem
is realted to partially applied type synomyms you described.

Thanks!
Dmitry

On Tue, Dec 6, 2011 at 10:59 PM, Dan Doel <dan.doel <at> gmail.com> wrote:
> Greetings,
>
> In the process of working on a Haskell-alike language recently, Ed
> Kmett and I realized that we had (without really thinking about it)
> implemented type synonyms that are a bit more liberal than GHC's. With
> LiberalTypeSynonyms enabled, GHC allows:
>
>    type Foo a b = b -> a
>    type Bar f = f String Int
>
>    baz :: Bar Foo
>    baz = show
>
> because Bar expands to saturate Foo. However, we had also implemented
> the following, which fails in GHC:
>
>    type Foo a b = b -> a
>    type Bar f = f (Foo Int) (Foo Int)
>    type Baz f g = f Int -> g Int
>
>    quux :: Bar Baz
>    quux = id
>
> That is: type synonyms are allowed to be partially applied within
> other type synonyms, as long as similar transitive saturation
> guarantees are met during their use.
>
> I don't know how useful it is, but I was curious if anyone can see
> anything wrong with allowing this (it seems okay to me after a little
> thought), and thought I'd float the idea out to the GHC developers, in
> case they're interested in picking it up.
>
> -- Dan
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe



--
Mvh Øystein Kolsrud

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Dmitry Kulagin | 7 Dec 12:38 2011
Picon

Re: More liberal than liberal type synonyms

> Dmitry, does your code work with LiberalTypeSynonyms extention activated?
No, the same error:
Type synonym `StateA' should have 1 argument, but has been given 0

But I have GHC 6.12.3

Dmitry
2011/12/7 Yves Parès <limestrael <at> gmail.com>:
> This is impossible:
> in the definition of 'StateT s m a', m must be a monad and then have the *
> -> * kind.
> So you cannot pass (StateA a), because it has simply the * kind.
>
> Dmitry, does your code work with LiberalTypeSynonyms extention activated?
>
>
> 2011/12/7 Øystein Kolsrud <kolsrud <at> gmail.com>
>>
>> You should be able to write something like this:
>>
>> type StateB a b = StateT SomeOtherState (StateA a) b
>>
>> Best regards, Øystein Kolsrud
>>
>>
>> On Wed, Dec 7, 2011 at 11:48 AM, Dmitry Kulagin <dmitry.kulagin <at> gmail.com>
>> wrote:
>>>
>>> Hi Dan,
>>>
>>> I am still pretty new in Haskell, but this problem annoys me already.
>>>
>>> If I define certain monad as a type synonym:
>>>
>>>    type StateA a = StateT SomeState SomeMonad a
>>>
>>> Then I can't declare new monad based on the synonym:
>>>
>>>    type StateB a = StateT SomeOtherState StateA a
>>>
>>> The only way I know to overcome is to declare StateA without `a':
>>>
>>>    type StateA = StateT SomeState SomeMonad
>>>
>>> But it is not always possible with existing code base.
>>>
>>> I am sorry, if this is offtopic, but it seemed to me that the problem
>>> is realted to partially applied type synomyms you described.
>>>
>>> Thanks!
>>> Dmitry
>>>
>>> On Tue, Dec 6, 2011 at 10:59 PM, Dan Doel <dan.doel <at> gmail.com> wrote:
>>> > Greetings,
>>> >
>>> > In the process of working on a Haskell-alike language recently, Ed
>>> > Kmett and I realized that we had (without really thinking about it)
>>> > implemented type synonyms that are a bit more liberal than GHC's. With
>>> > LiberalTypeSynonyms enabled, GHC allows:
>>> >
>>> >    type Foo a b = b -> a
>>> >    type Bar f = f String Int
>>> >
>>> >    baz :: Bar Foo
>>> >    baz = show
>>> >
>>> > because Bar expands to saturate Foo. However, we had also implemented
>>> > the following, which fails in GHC:
>>> >
>>> >    type Foo a b = b -> a
>>> >    type Bar f = f (Foo Int) (Foo Int)
>>> >    type Baz f g = f Int -> g Int
>>> >
>>> >    quux :: Bar Baz
>>> >    quux = id
>>> >
>>> > That is: type synonyms are allowed to be partially applied within
>>> > other type synonyms, as long as similar transitive saturation
>>> > guarantees are met during their use.
>>> >
>>> > I don't know how useful it is, but I was curious if anyone can see
>>> > anything wrong with allowing this (it seems okay to me after a little
>>> > thought), and thought I'd float the idea out to the GHC developers, in
>>> > case they're interested in picking it up.
>>> >
>>> > -- Dan
>>> >
>>> > _______________________________________________
>>> > Haskell-Cafe mailing list
>>> > Haskell-Cafe <at> haskell.org
>>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe <at> haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>>
>>
>> --
>> Mvh Øystein Kolsrud
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe <at> haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
Yves Parès | 7 Dec 12:51 2011
Picon

Re: More liberal than liberal type synonyms

Ah, maybe Dan could tell us if it works only with GHC 7.

Dmitry, I had your problem many times. The last time was when I saw you could define the ContT monad in terms of Cont (the opposite is done in the mtl).
It leads to a simpler code, but you are stucked when trying to define ContT as an instance of MonadTrans:

data Cont r a = ...
-- [instances of Monad Cont, blah blah blah]

type ContT r m a = Cont r (m a)

instance MonadTrans (ContT r) where  -- This doesn't compile, even if it is logical
  lift = ...

For short, type synonyms work for mere aliases, but not for full-fledged type-level non-inductive functions.
And sometimes we intuitively want to use them as such.

2011/12/7 Dmitry Kulagin <dmitry.kulagin <at> gmail.com>
> Dmitry, does your code work with LiberalTypeSynonyms extention activated?
No, the same error:
Type synonym `StateA' should have 1 argument, but has been given 0

But I have GHC 6.12.3

Dmitry
2011/12/7 Yves Parès <limestrael <at> gmail.com>:
> This is impossible:
> in the definition of 'StateT s m a', m must be a monad and then have the *
> -> * kind.
> So you cannot pass (StateA a), because it has simply the * kind.
>
> Dmitry, does your code work with LiberalTypeSynonyms extention activated?
>
>
> 2011/12/7 Øystein Kolsrud <kolsrud <at> gmail.com>
>>
>> You should be able to write something like this:
>>
>> type StateB a b = StateT SomeOtherState (StateA a) b
>>
>> Best regards, Øystein Kolsrud
>>
>>
>> On Wed, Dec 7, 2011 at 11:48 AM, Dmitry Kulagin <dmitry.kulagin <at> gmail.com>
>> wrote:
>>>
>>> Hi Dan,
>>>
>>> I am still pretty new in Haskell, but this problem annoys me already.
>>>
>>> If I define certain monad as a type synonym:
>>>
>>>    type StateA a = StateT SomeState SomeMonad a
>>>
>>> Then I can't declare new monad based on the synonym:
>>>
>>>    type StateB a = StateT SomeOtherState StateA a
>>>
>>> The only way I know to overcome is to declare StateA without `a':
>>>
>>>    type StateA = StateT SomeState SomeMonad
>>>
>>> But it is not always possible with existing code base.
>>>
>>> I am sorry, if this is offtopic, but it seemed to me that the problem
>>> is realted to partially applied type synomyms you described.
>>>
>>> Thanks!
>>> Dmitry
>>>
>>> On Tue, Dec 6, 2011 at 10:59 PM, Dan Doel <dan.doel <at> gmail.com> wrote:
>>> > Greetings,
>>> >
>>> > In the process of working on a Haskell-alike language recently, Ed
>>> > Kmett and I realized that we had (without really thinking about it)
>>> > implemented type synonyms that are a bit more liberal than GHC's. With
>>> > LiberalTypeSynonyms enabled, GHC allows:
>>> >
>>> >    type Foo a b = b -> a
>>> >    type Bar f = f String Int
>>> >
>>> >    baz :: Bar Foo
>>> >    baz = show
>>> >
>>> > because Bar expands to saturate Foo. However, we had also implemented
>>> > the following, which fails in GHC:
>>> >
>>> >    type Foo a b = b -> a
>>> >    type Bar f = f (Foo Int) (Foo Int)
>>> >    type Baz f g = f Int -> g Int
>>> >
>>> >    quux :: Bar Baz
>>> >    quux = id
>>> >
>>> > That is: type synonyms are allowed to be partially applied within
>>> > other type synonyms, as long as similar transitive saturation
>>> > guarantees are met during their use.
>>> >
>>> > I don't know how useful it is, but I was curious if anyone can see
>>> > anything wrong with allowing this (it seems okay to me after a little
>>> > thought), and thought I'd float the idea out to the GHC developers, in
>>> > case they're interested in picking it up.
>>> >
>>> > -- Dan
>>> >
>>> > _______________________________________________
>>> > Haskell-Cafe mailing list
>>> > Haskell-Cafe <at> haskell.org
>>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe <at> haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>>
>>
>> --
>> Mvh Øystein Kolsrud
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe <at> haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Dmitry Kulagin | 7 Dec 13:07 2011
Picon

Re: More liberal than liberal type synonyms

> For short, type synonyms work for mere aliases, but not for full-fledged> type-level non-inductive
functions.> And sometimes we intuitively want to use them as such.
Thank you, Yves! It is now more clear for me.

Still, it seems that ability to use partially applied type synonyms would be
very natural (and useful) extension to the language. It would allow to avoid
boilerplate code associated with creating "really new" types instead of just
using synonims for existing ones.

On Wed, Dec 7, 2011 at 3:51 PM, Yves Parès <limestrael <at> gmail.com> wrote:
> Ah, maybe Dan could tell us if it works only with GHC 7.
>
> Dmitry, I had your problem many times. The last time was when I saw you
> could define the ContT monad in terms of Cont (the opposite is done in the
> mtl).
> It leads to a simpler code, but you are stucked when trying to define ContT
> as an instance of MonadTrans:
>
> data Cont r a = ...
> -- [instances of Monad Cont, blah blah blah]
>
> type ContT r m a = Cont r (m a)
>
> instance MonadTrans (ContT r) where  -- This doesn't compile, even if it is
> logical
>   lift = ...
>
> For short, type synonyms work for mere aliases, but not for full-fledged
> type-level non-inductive functions.
> And sometimes we intuitively want to use them as such.
>
>
> 2011/12/7 Dmitry Kulagin <dmitry.kulagin <at> gmail.com>
>>
>> > Dmitry, does your code work with LiberalTypeSynonyms extention
>> > activated?
>> No, the same error:
>> Type synonym `StateA' should have 1 argument, but has been given 0
>>
>> But I have GHC 6.12.3
>>
>> Dmitry
>> 2011/12/7 Yves Parès <limestrael <at> gmail.com>:
>> > This is impossible:
>> > in the definition of 'StateT s m a', m must be a monad and then have the
>> > *
>> > -> * kind.
>> > So you cannot pass (StateA a), because it has simply the * kind.
>> >
>> > Dmitry, does your code work with LiberalTypeSynonyms extention
>> > activated?
>> >
>> >
>> > 2011/12/7 Øystein Kolsrud <kolsrud <at> gmail.com>
>> >>
>> >> You should be able to write something like this:
>> >>
>> >> type StateB a b = StateT SomeOtherState (StateA a) b
>> >>
>> >> Best regards, Øystein Kolsrud
>> >>
>> >>
>> >> On Wed, Dec 7, 2011 at 11:48 AM, Dmitry Kulagin
>> >> <dmitry.kulagin <at> gmail.com>
>> >> wrote:
>> >>>
>> >>> Hi Dan,
>> >>>
>> >>> I am still pretty new in Haskell, but this problem annoys me already.
>> >>>
>> >>> If I define certain monad as a type synonym:
>> >>>
>> >>>    type StateA a = StateT SomeState SomeMonad a
>> >>>
>> >>> Then I can't declare new monad based on the synonym:
>> >>>
>> >>>    type StateB a = StateT SomeOtherState StateA a
>> >>>
>> >>> The only way I know to overcome is to declare StateA without `a':
>> >>>
>> >>>    type StateA = StateT SomeState SomeMonad
>> >>>
>> >>> But it is not always possible with existing code base.
>> >>>
>> >>> I am sorry, if this is offtopic, but it seemed to me that the problem
>> >>> is realted to partially applied type synomyms you described.
>> >>>
>> >>> Thanks!
>> >>> Dmitry
>> >>>
>> >>> On Tue, Dec 6, 2011 at 10:59 PM, Dan Doel <dan.doel <at> gmail.com> wrote:
>> >>> > Greetings,
>> >>> >
>> >>> > In the process of working on a Haskell-alike language recently, Ed
>> >>> > Kmett and I realized that we had (without really thinking about it)
>> >>> > implemented type synonyms that are a bit more liberal than GHC's.
>> >>> > With
>> >>> > LiberalTypeSynonyms enabled, GHC allows:
>> >>> >
>> >>> >    type Foo a b = b -> a
>> >>> >    type Bar f = f String Int
>> >>> >
>> >>> >    baz :: Bar Foo
>> >>> >    baz = show
>> >>> >
>> >>> > because Bar expands to saturate Foo. However, we had also
>> >>> > implemented
>> >>> > the following, which fails in GHC:
>> >>> >
>> >>> >    type Foo a b = b -> a
>> >>> >    type Bar f = f (Foo Int) (Foo Int)
>> >>> >    type Baz f g = f Int -> g Int
>> >>> >
>> >>> >    quux :: Bar Baz
>> >>> >    quux = id
>> >>> >
>> >>> > That is: type synonyms are allowed to be partially applied within
>> >>> > other type synonyms, as long as similar transitive saturation
>> >>> > guarantees are met during their use.
>> >>> >
>> >>> > I don't know how useful it is, but I was curious if anyone can see
>> >>> > anything wrong with allowing this (it seems okay to me after a
>> >>> > little
>> >>> > thought), and thought I'd float the idea out to the GHC developers,
>> >>> > in
>> >>> > case they're interested in picking it up.
>> >>> >
>> >>> > -- Dan
>> >>> >
>> >>> > _______________________________________________
>> >>> > Haskell-Cafe mailing list
>> >>> > Haskell-Cafe <at> haskell.org
>> >>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >>>
>> >>> _______________________________________________
>> >>> Haskell-Cafe mailing list
>> >>> Haskell-Cafe <at> haskell.org
>> >>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >>
>> >>
>> >>
>> >>
>> >> --
>> >> Mvh Øystein Kolsrud
>> >>
>> >> _______________________________________________
>> >> Haskell-Cafe mailing list
>> >> Haskell-Cafe <at> haskell.org
>> >> http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >>
>> >
>
>
Gábor Lehel | 7 Dec 16:47 2011
Picon

Re: More liberal than liberal type synonyms

On Wed, Dec 7, 2011 at 1:07 PM, Dmitry Kulagin <dmitry.kulagin <at> gmail.com> wrote:
>> For short, type synonyms work for mere aliases, but not for full-fledged> type-level non-inductive
functions.> And sometimes we intuitively want to use them as such.
> Thank you, Yves! It is now more clear for me.
>
> Still, it seems that ability to use partially applied type synonyms would be
> very natural (and useful) extension to the language. It would allow to avoid
> boilerplate code associated with creating "really new" types instead of just
> using synonims for existing ones.

The problem as I understand it is that partially-applied type synonyms
are in effect type level lambdas, and type checking in the presence of
type level lambdas requires higher-order unification, which is
undecidable in general. Restricted cases might be possible, I'm not an
expert in the field. GHC hackers could probably elaborate.

[1] http://stackoverflow.com/questions/8248217/are-there-type-level-combinators-will-they-exist-in-some-future
[2] http://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification

>
> On Wed, Dec 7, 2011 at 3:51 PM, Yves Parès <limestrael <at> gmail.com> wrote:
>> Ah, maybe Dan could tell us if it works only with GHC 7.
>>
>> Dmitry, I had your problem many times. The last time was when I saw you
>> could define the ContT monad in terms of Cont (the opposite is done in the
>> mtl).
>> It leads to a simpler code, but you are stucked when trying to define ContT
>> as an instance of MonadTrans:
>>
>> data Cont r a = ...
>> -- [instances of Monad Cont, blah blah blah]
>>
>> type ContT r m a = Cont r (m a)
>>
>> instance MonadTrans (ContT r) where  -- This doesn't compile, even if it is
>> logical
>>   lift = ...
>>
>> For short, type synonyms work for mere aliases, but not for full-fledged
>> type-level non-inductive functions.
>> And sometimes we intuitively want to use them as such.
>>
>>
>> 2011/12/7 Dmitry Kulagin <dmitry.kulagin <at> gmail.com>
>>>
>>> > Dmitry, does your code work with LiberalTypeSynonyms extention
>>> > activated?
>>> No, the same error:
>>> Type synonym `StateA' should have 1 argument, but has been given 0
>>>
>>> But I have GHC 6.12.3
>>>
>>> Dmitry
>>> 2011/12/7 Yves Parès <limestrael <at> gmail.com>:
>>> > This is impossible:
>>> > in the definition of 'StateT s m a', m must be a monad and then have the
>>> > *
>>> > -> * kind.
>>> > So you cannot pass (StateA a), because it has simply the * kind.
>>> >
>>> > Dmitry, does your code work with LiberalTypeSynonyms extention
>>> > activated?
>>> >
>>> >
>>> > 2011/12/7 Øystein Kolsrud <kolsrud <at> gmail.com>
>>> >>
>>> >> You should be able to write something like this:
>>> >>
>>> >> type StateB a b = StateT SomeOtherState (StateA a) b
>>> >>
>>> >> Best regards, Øystein Kolsrud
>>> >>
>>> >>
>>> >> On Wed, Dec 7, 2011 at 11:48 AM, Dmitry Kulagin
>>> >> <dmitry.kulagin <at> gmail.com>
>>> >> wrote:
>>> >>>
>>> >>> Hi Dan,
>>> >>>
>>> >>> I am still pretty new in Haskell, but this problem annoys me already.
>>> >>>
>>> >>> If I define certain monad as a type synonym:
>>> >>>
>>> >>>    type StateA a = StateT SomeState SomeMonad a
>>> >>>
>>> >>> Then I can't declare new monad based on the synonym:
>>> >>>
>>> >>>    type StateB a = StateT SomeOtherState StateA a
>>> >>>
>>> >>> The only way I know to overcome is to declare StateA without `a':
>>> >>>
>>> >>>    type StateA = StateT SomeState SomeMonad
>>> >>>
>>> >>> But it is not always possible with existing code base.
>>> >>>
>>> >>> I am sorry, if this is offtopic, but it seemed to me that the problem
>>> >>> is realted to partially applied type synomyms you described.
>>> >>>
>>> >>> Thanks!
>>> >>> Dmitry
>>> >>>
>>> >>> On Tue, Dec 6, 2011 at 10:59 PM, Dan Doel <dan.doel <at> gmail.com> wrote:
>>> >>> > Greetings,
>>> >>> >
>>> >>> > In the process of working on a Haskell-alike language recently, Ed
>>> >>> > Kmett and I realized that we had (without really thinking about it)
>>> >>> > implemented type synonyms that are a bit more liberal than GHC's.
>>> >>> > With
>>> >>> > LiberalTypeSynonyms enabled, GHC allows:
>>> >>> >
>>> >>> >    type Foo a b = b -> a
>>> >>> >    type Bar f = f String Int
>>> >>> >
>>> >>> >    baz :: Bar Foo
>>> >>> >    baz = show
>>> >>> >
>>> >>> > because Bar expands to saturate Foo. However, we had also
>>> >>> > implemented
>>> >>> > the following, which fails in GHC:
>>> >>> >
>>> >>> >    type Foo a b = b -> a
>>> >>> >    type Bar f = f (Foo Int) (Foo Int)
>>> >>> >    type Baz f g = f Int -> g Int
>>> >>> >
>>> >>> >    quux :: Bar Baz
>>> >>> >    quux = id
>>> >>> >
>>> >>> > That is: type synonyms are allowed to be partially applied within
>>> >>> > other type synonyms, as long as similar transitive saturation
>>> >>> > guarantees are met during their use.
>>> >>> >
>>> >>> > I don't know how useful it is, but I was curious if anyone can see
>>> >>> > anything wrong with allowing this (it seems okay to me after a
>>> >>> > little
>>> >>> > thought), and thought I'd float the idea out to the GHC developers,
>>> >>> > in
>>> >>> > case they're interested in picking it up.
>>> >>> >
>>> >>> > -- Dan
>>> >>> >
>>> >>> > _______________________________________________
>>> >>> > Haskell-Cafe mailing list
>>> >>> > Haskell-Cafe <at> haskell.org
>>> >>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>>> >>>
>>> >>> _______________________________________________
>>> >>> Haskell-Cafe mailing list
>>> >>> Haskell-Cafe <at> haskell.org
>>> >>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>> >>
>>> >>
>>> >>
>>> >>
>>> >> --
>>> >> Mvh Øystein Kolsrud
>>> >>
>>> >> _______________________________________________
>>> >> Haskell-Cafe mailing list
>>> >> Haskell-Cafe <at> haskell.org
>>> >> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>> >>
>>> >
>>
>>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

--

-- 
Work is punishment for failing to procrastinate effectively.
Brent Yorgey | 8 Dec 19:50 2011

Re: More liberal than liberal type synonyms

On Wed, Dec 07, 2011 at 04:47:47PM +0100, Gábor Lehel wrote:
> On Wed, Dec 7, 2011 at 1:07 PM, Dmitry Kulagin <dmitry.kulagin <at> gmail.com> wrote:
> >> For short, type synonyms work for mere aliases, but not for full-fledged> type-level non-inductive
functions.> And sometimes we intuitively want to use them as such.
> > Thank you, Yves! It is now more clear for me.
> >
> > Still, it seems that ability to use partially applied type synonyms would be
> > very natural (and useful) extension to the language. It would allow to avoid
> > boilerplate code associated with creating "really new" types instead of just
> > using synonims for existing ones.
> 
> The problem as I understand it is that partially-applied type synonyms
> are in effect type level lambdas, and type checking in the presence of
> type level lambdas requires higher-order unification, which is
> undecidable in general. Restricted cases might be possible, I'm not an
> expert in the field. GHC hackers could probably elaborate.
> 
> [1] http://stackoverflow.com/questions/8248217/are-there-type-level-combinators-will-they-exist-in-some-future
> [2]
> http://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification

It's actually type *inference* that requires higher-order unification
in the presence of type-level lambdas, not type checking.  This might
not be a huge deal: we just have to clearly state that enabling
-XPartialTypeFunApps means that you may have to provide some explicit
type annotations in places where type inference cannot figure things
out.  We already have extensions like this (e.g. RankNTypes).

The bigger problem for the moment is that for various technical
reasons, enabling partial applications of type functions can lead to
unsoundness (i.e. typechecked programs which nonetheless crash at
runtime) in the way that type equality is handled.  For more details
see 

  http://stackoverflow.com/questions/7866375/why-does-ghc-think-that-this-type-variable-is-not-injective/7950614#7950614

I agree that the ability to use partially applied type
synonyms/functions would be natural and useful.  I hope we will
eventually see a version of GHC which supports it but there are some
nontrivial technical issues to be worked out first.

-Brent

> 
> >
> > On Wed, Dec 7, 2011 at 3:51 PM, Yves Parès <limestrael <at> gmail.com> wrote:
> >> Ah, maybe Dan could tell us if it works only with GHC 7.
> >>
> >> Dmitry, I had your problem many times. The last time was when I saw you
> >> could define the ContT monad in terms of Cont (the opposite is done in the
> >> mtl).
> >> It leads to a simpler code, but you are stucked when trying to define ContT
> >> as an instance of MonadTrans:
> >>
> >> data Cont r a = ...
> >> -- [instances of Monad Cont, blah blah blah]
> >>
> >> type ContT r m a = Cont r (m a)
> >>
> >> instance MonadTrans (ContT r) where  -- This doesn't compile, even if it is
> >> logical
> >>   lift = ...
> >>
> >> For short, type synonyms work for mere aliases, but not for full-fledged
> >> type-level non-inductive functions.
> >> And sometimes we intuitively want to use them as such.
> >>
> >>
> >> 2011/12/7 Dmitry Kulagin <dmitry.kulagin <at> gmail.com>
> >>>
> >>> > Dmitry, does your code work with LiberalTypeSynonyms extention
> >>> > activated?
> >>> No, the same error:
> >>> Type synonym `StateA' should have 1 argument, but has been given 0
> >>>
> >>> But I have GHC 6.12.3
> >>>
> >>> Dmitry
> >>> 2011/12/7 Yves Parès <limestrael <at> gmail.com>:
> >>> > This is impossible:
> >>> > in the definition of 'StateT s m a', m must be a monad and then have the
> >>> > *
> >>> > -> * kind.
> >>> > So you cannot pass (StateA a), because it has simply the * kind.
> >>> >
> >>> > Dmitry, does your code work with LiberalTypeSynonyms extention
> >>> > activated?
> >>> >
> >>> >
> >>> > 2011/12/7 Øystein Kolsrud <kolsrud <at> gmail.com>
> >>> >>
> >>> >> You should be able to write something like this:
> >>> >>
> >>> >> type StateB a b = StateT SomeOtherState (StateA a) b
> >>> >>
> >>> >> Best regards, Øystein Kolsrud
> >>> >>
> >>> >>
> >>> >> On Wed, Dec 7, 2011 at 11:48 AM, Dmitry Kulagin
> >>> >> <dmitry.kulagin <at> gmail.com>
> >>> >> wrote:
> >>> >>>
> >>> >>> Hi Dan,
> >>> >>>
> >>> >>> I am still pretty new in Haskell, but this problem annoys me already.
> >>> >>>
> >>> >>> If I define certain monad as a type synonym:
> >>> >>>
> >>> >>>    type StateA a = StateT SomeState SomeMonad a
> >>> >>>
> >>> >>> Then I can't declare new monad based on the synonym:
> >>> >>>
> >>> >>>    type StateB a = StateT SomeOtherState StateA a
> >>> >>>
> >>> >>> The only way I know to overcome is to declare StateA without `a':
> >>> >>>
> >>> >>>    type StateA = StateT SomeState SomeMonad
> >>> >>>
> >>> >>> But it is not always possible with existing code base.
> >>> >>>
> >>> >>> I am sorry, if this is offtopic, but it seemed to me that the problem
> >>> >>> is realted to partially applied type synomyms you described.
> >>> >>>
> >>> >>> Thanks!
> >>> >>> Dmitry
> >>> >>>
> >>> >>> On Tue, Dec 6, 2011 at 10:59 PM, Dan Doel <dan.doel <at> gmail.com> wrote:
> >>> >>> > Greetings,
> >>> >>> >
> >>> >>> > In the process of working on a Haskell-alike language recently, Ed
> >>> >>> > Kmett and I realized that we had (without really thinking about it)
> >>> >>> > implemented type synonyms that are a bit more liberal than GHC's.
> >>> >>> > With
> >>> >>> > LiberalTypeSynonyms enabled, GHC allows:
> >>> >>> >
> >>> >>> >    type Foo a b = b -> a
> >>> >>> >    type Bar f = f String Int
> >>> >>> >
> >>> >>> >    baz :: Bar Foo
> >>> >>> >    baz = show
> >>> >>> >
> >>> >>> > because Bar expands to saturate Foo. However, we had also
> >>> >>> > implemented
> >>> >>> > the following, which fails in GHC:
> >>> >>> >
> >>> >>> >    type Foo a b = b -> a
> >>> >>> >    type Bar f = f (Foo Int) (Foo Int)
> >>> >>> >    type Baz f g = f Int -> g Int
> >>> >>> >
> >>> >>> >    quux :: Bar Baz
> >>> >>> >    quux = id
> >>> >>> >
> >>> >>> > That is: type synonyms are allowed to be partially applied within
> >>> >>> > other type synonyms, as long as similar transitive saturation
> >>> >>> > guarantees are met during their use.
> >>> >>> >
> >>> >>> > I don't know how useful it is, but I was curious if anyone can see
> >>> >>> > anything wrong with allowing this (it seems okay to me after a
> >>> >>> > little
> >>> >>> > thought), and thought I'd float the idea out to the GHC developers,
> >>> >>> > in
> >>> >>> > case they're interested in picking it up.
> >>> >>> >
> >>> >>> > -- Dan
> >>> >>> >
> >>> >>> > _______________________________________________
> >>> >>> > Haskell-Cafe mailing list
> >>> >>> > Haskell-Cafe <at> haskell.org
> >>> >>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >>> >>>
> >>> >>> _______________________________________________
> >>> >>> Haskell-Cafe mailing list
> >>> >>> Haskell-Cafe <at> haskell.org
> >>> >>> http://www.haskell.org/mailman/listinfo/haskell-cafe
> >>> >>
> >>> >>
> >>> >>
> >>> >>
> >>> >> --
> >>> >> Mvh Øystein Kolsrud
> >>> >>
> >>> >> _______________________________________________
> >>> >> Haskell-Cafe mailing list
> >>> >> Haskell-Cafe <at> haskell.org
> >>> >> http://www.haskell.org/mailman/listinfo/haskell-cafe
> >>> >>
> >>> >
> >>
> >>
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe <at> haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
> 
> 
> -- 
> Work is punishment for failing to procrastinate effectively.
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
Dan Doel | 7 Dec 17:19 2011
Picon

Re: [Haskell-cafe] More liberal than liberal type synonyms

On Wed, Dec 7, 2011 at 5:48 AM, Dmitry Kulagin <dmitry.kulagin <at> gmail.com> wrote:
> I am still pretty new in Haskell, but this problem annoys me already.
>
> If I define certain monad as a type synonym:
>
>    type StateA a = StateT SomeState SomeMonad a
>
> Then I can't declare new monad based on the synonym:
>
>    type StateB a = StateT SomeOtherState StateA a
>
> The only way I know to overcome is to declare StateA without `a':
>
>    type StateA = StateT SomeState SomeMonad
>
> But it is not always possible with existing code base.

I'm afraid my proposal doesn't make this work. You could perhaps
define StateB, but when you expand in a type you get:

    StateB a = StateT SomeOtherState StateA a

which has a partially applied StateA, and is rejected. The only way to
make this work is to eta reduce StateA manually, or make GHC recognize
when a synonym can be eta reduced in this way (which might be both
possible and useful as a separate proposal).

My extension fell within the liberal type synonym space, which says
that if you have:

    F G

where F and G are both synonyms, and G is partially applied, then it
is okay as long as expansion of F (and any subsequent expansions)
cause G to become fully applied. My extension of this is just to allow
partial application inside aliases as long as it meets these same
criteria.

The reason to disallow partially applied type aliases is that they
make inference pretty much impossible, unless you only infer them in
very limited circumstances perhaps. And if you can't get inference of
them, you probably need to start having explicit annotations to tell
the type checker what you want to happen, which has some of its own
complications with the way quantifiers work in GHC and such. It'd
cascade into some thorny issues.

Hopefully that covers all the other subsequent stuff folks have been
talking about.

-- Dan

Gmane