Which stable GHC release is expected to have support for linear types?

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

Re: Which stable GHC release is expected to have support for linear types?

Brandon Allbery
On Wed, Jul 12, 2017 at 4:11 PM, Wolfgang Jeltsch <[hidden email]> wrote:
I had thought about this possibility already, but then concluded that this was not the case, since types of the form a -o b were not supported. However, when looking at the diffs, I discovered that at the moment, only the Unicode syntax a ⊸ b is understood.

"-o" is going to give the lexer fits. Come up with a purely symbolic version. 

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Wolfgang Jeltsch-3
Am Mittwoch, den 12.07.2017, 16:15 -0400 schrieb Brandon Allbery:
On Wed, Jul 12, 2017 at 4:11 PM, Wolfgang Jeltsch <[hidden email]> wrote:
I had thought about this possibility already, but then concluded that this was not the case, since types of the form a -o b were not supported. However, when looking at the diffs, I discovered that at the moment, only the Unicode syntax a ⊸ b is understood.

"-o" is going to give the lexer fits. Come up with a purely symbolic version.

It was not me who invented the syntax “-o”. Actually, I do not like it either. While it nicely resembles the lollipop (⊸), implementing it requires stealing syntax. This syntax stealing is worse than the syntax stealing of, say, hierarchical modules. With hierarchical modules in place, you have to use spaces in function composition, but this is reasonable anyhow. However, with “-o” as a lollipop alternative in place, you have to write the negation of o with a space, which is awkward.

Alternatives for “-o” I can think of are “~>”, “-:”, and “-*”, the latter resembling the magic wand operators in the logic of bunched implications and in separation logic, which are similar to the lollipop in linear logic.

All the best,
Wolfgang

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Joachim Breitner-2
Hi,

Am Mittwoch, den 12.07.2017, 23:47 +0300 schrieb Wolfgang Jeltsch:
> Alternatives for “-o” I can think of are “~>”, “-:”, and “-*”, the
> latter resembling the magic wand operators in the logic of bunched
> implications and in separation logic, which are similar to the
> lollipop in linear logic.

how about -<> ?

Joachim
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Wolfgang Jeltsch-3
Am Donnerstag, den 13.07.2017, 11:03 +0200 schrieb Joachim Breitner:
> Am Mittwoch, den 12.07.2017, 23:47 +0300 schrieb Wolfgang Jeltsch:
> > Alternatives for “-o” I can think of are “~>”, “-:”, and “-*”, the
> > latter resembling the magic wand operators in the logic of bunched
> > implications and in separation logic, which are similar to the
> > lollipop in linear logic.
>
> how about -<> ?

Hmm, the “<>” part seems to be a bit heavy compared to the little “-”.

All the best,
Wolfgang
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Mike Ledger
How about: -+

It almost looks arrow like if you squint, and have a font that lines up the horizontal lines.

Cheers,
Mike


On 14 Jul 2017 08:32, "Wolfgang Jeltsch" <[hidden email]> wrote:
Am Donnerstag, den 13.07.2017, 11:03 +0200 schrieb Joachim Breitner:
> Am Mittwoch, den 12.07.2017, 23:47 +0300 schrieb Wolfgang Jeltsch:
> > Alternatives for “-o” I can think of are “~>”, “-:”, and “-*”, the
> > latter resembling the magic wand operators in the logic of bunched
> > implications and in separation logic, which are similar to the
> > lollipop in linear logic.
>
> how about -<> ?

Hmm, the “<>” part seems to be a bit heavy compared to the little “-”.

All the best,
Wolfgang
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Wolfgang Jeltsch-3
Am Freitag, den 14.07.2017, 09:26 +1000 schrieb Mike Ledger:
How about: -+

It almost looks arrow like if you squint, and have a font that lines up the horizontal lines.

Interesting idea. Seems pretty good to me. It does not only look arrow-like, but also similar to the lollipop (⊸).

Let’s try it out:

fmap :: Functor f => (a -+ b) -> f a -+ f b

Yes, this looks quite nice. Let’s compare it to the Unicode version:

fmap ∷ Functor f ⇒ (a ⊸ b) → (f a ⊸ f b)

They look similar indeed. 😉

All the best,
Wolfgang

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Bardur Arantsson-2
In reply to this post by Mike Ledger
On 2017-07-14 01:26, Mike Ledger wrote:
> How about: -+
>
> It almost looks arrow like if you squint, and have a font that lines up
> the horizontal lines.
>

This may play havoc with programming fonts with ligatures where it might
be rendered as a single ± symbol.

(I haven't tested any of the fonts, I'm just saying it _could_ be an issue.)

Regards,

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Wolfgang Jeltsch-3
Am Freitag, den 14.07.2017, 06:42 +0200 schrieb Bardur Arantsson:

> On 2017-07-14 01:26, Mike Ledger wrote:
> > How about: -+
> >
> > It almost looks arrow like if you squint, and have a font that lines
> > up the horizontal lines.
>
> This may play havoc with programming fonts with ligatures where it
> might be rendered as a single ± symbol.
>
> (I haven't tested any of the fonts, I'm just saying it _could_ be an
> issue.)

I would expect such fonts to translate “+-”, not “-+”, into “±”.

All the best,
Wolfgang
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Bardur Arantsson-2
On 2017-07-14 21:59, Wolfgang Jeltsch wrote:

> Am Freitag, den 14.07.2017, 06:42 +0200 schrieb Bardur Arantsson:
>> On 2017-07-14 01:26, Mike Ledger wrote:
>>> How about: -+
>>>
>>> It almost looks arrow like if you squint, and have a font that lines
>>> up the horizontal lines.
>>
>> This may play havoc with programming fonts with ligatures where it
>> might be rendered as a single ± symbol.
>>
>> (I haven't tested any of the fonts, I'm just saying it _could_ be an
>> issue.)
>
> I would expect such fonts to translate “+-”, not “-+”, into “±”.
>

Maybe, but it seems a bit fragile to me...

What about -*? At least there's no ambiguity there.

Regards,

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Brandon Allbery
On Sat, Jul 15, 2017 at 4:57 AM, Bardur Arantsson <[hidden email]> wrote:
Maybe, but it seems a bit fragile to me...

What about -*? At least there's no ambiguity there.

As previously stated: "Alternatives for “-o” I can think of are “~>”, “-:”, and “-*”, the latter resembling the magic wand operators in the logic of bunched implications and in separation logic, which are similar to the lollipop in linear logic." 

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Which stable GHC release is expected to have support for linear types?

Wolfgang Jeltsch-3
In reply to this post by Bardur Arantsson-2
Am Samstag, den 15.07.2017, 10:57 +0200 schrieb Bardur Arantsson:

> On 2017-07-14 21:59, Wolfgang Jeltsch wrote:
> > Am Freitag, den 14.07.2017, 06:42 +0200 schrieb Bardur Arantsson:
> > > On 2017-07-14 01:26, Mike Ledger wrote:
> > > > How about: -+
> > > >
> > > > It almost looks arrow like if you squint, and have a font that
> > > > lines up the horizontal lines.
> > >
> > > This may play havoc with programming fonts with ligatures where it
> > > might be rendered as a single ± symbol.
> > > 
> > I would expect such fonts to translate “+-”, not “-+”, into “±”.
> >
> Maybe, but it seems a bit fragile to me...

I would not care too much about such fonts. In my opinion, the natural
way is to generate ± from +-, not from -+. Since there is the option to
generate ± from +-, there is no need to additionally generate it
from -+. Font designers could just stop doing this if there are doing it
at all at the moment.

> What about -*? At least there's no ambiguity there.

The problem with -* is that the star is typically higher than the -, so
that -* looks a bit awkward.

I think, using -+ is a pretty good idea.

All the best,
Wolfgang
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
12