Re: [racket-users] Typed Racket & Higher Kinded Types

[Anthony Carrico]

On 01/17/2017 04:34 AM, Sam Tobin-Hochstadt wrote:
> No, unfortunately  you can't just higher kinds in Typed Racket. This is
> a limitation we hope to lift eventually, though.

I'm going to take a non-ranting stab at Matthias' compatibility
objection, slightly formalizing the proposal. Robert wants kinds. I'll
use a syntax like:

Value : Type : Kind

Let's say we have these kinds:

Kind := * | (-> * *)

In #lang racket, there is only one type:

_ : Racket : *

So, use it for the Racket FFI. Initially, don't try to map uni-typed
Racket values onto a variety of types as Typed Racket did.

We probably also want to interop with C, so add a C FFI:

_ : C : *

We might have a type for #lang typed/racket too:

_ : Typed/Racket : ?

I don't know if you'd use  kind * here.

Later, it might be that we can do better than these types, as Typed
Racket did. In those cases people could add better types, but maybe
refinement isn't something that will work well in this kinded
programming model. Oh well, just use elimination forms on the Racket type.

Typed Racket is a world designed to make Schemer's
set/predicate/refinement model feel natural. Robert's #lang kind/racket,
or whatever, is a world designed to make static higher kinded typed
programming feel natural. As with any #lang, they live in the same heap,
and they don't have a perfect semantic match.

Sam, why do you characterize higher kinds in typed/racket as a
"limitation we hope to lift eventually" rather than just a design choice
for that #lang?

I understand that there are issues with the N*N combinatorial explosion
of languages, but that is something we just have to deal with by
grouping languages with shallow semantic differences into a single FFI,
or by documenting the mappings, like when you model a lazy application
with a thunk, or whatever.

-- 
Anthony Carrico

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Vincent St-Amour]

On Thu, 19 Jan 2017 10:42:17 -0600,
Robert Kuzelj wrote:
> 
> As far as I understand Haskell was breaking compatibility now then to
> add new languae features. This enabled the fast iteration (albeit a
> painful one).
> On the other hand F# is the exact opposite - not only looking to
> remain compatible to itself but also to the rest of the .NET eco
> system (and C#). All of that makes the progress of the language pretty
> slow (from my POV) and creates lots of warts that are not necessary if
> you are not into C#.

Unlike these, Racket has #lang, so you can have your cake and eat it too. :)

Vincent

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Robert Kuzelj]

Am Donnerstag, 19. Januar 2017 17:17:18 UTC+1 schrieb Matthias Felleisen:
> In case my CPSing obscured the prose, here is what I said: 
> 
> What I am really saying is that I supplemented the proposal with a research 
> challenge that is common in the Racket world. If you are here and you see the 
> blueprints for paradise over there, don’t just build paradise. Also build the 
> bridge from here to there. 

Just as a lurker into Racket for now - Is that really sensible? Always? I 
understand that the Racket culture might strongly lean into that but then ...

As far as I understand Haskell was breaking compatibility now then to add new 
languae features. This enabled the fast iteration (albeit a painful one).
On the other hand F# is the exact opposite - not only looking to remain 
compatible to itself but also to the rest of the .NET eco system (and C#). All 
of that makes the progress of the language pretty slow (from my POV) and 
creates lots of warts that are not necessary if you are not into C#.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Matthias Felleisen]

In case my CPSing obscured the prose, here is what I said: 

What I am really saying is that I supplemented the proposal with a research 
challenge that is common in the Racket world. If you are here and you see the 
blueprints for paradise over there, don’t just build paradise. Also build the 
bridge from here to there. 




> On Jan 19, 2017, at 10:57 AM, Matthias Felleisen  wrote:
> 
> 
> You’re preaching to the choir. See Racket Manifesto. 
> 
> But you’re also preaching to the guy who got this project to
> where it is because "Types Suck” has been my slogan for decades. 
> (I will leave it to figure out what that slogan means.) 
> 
> Since I am not a good programmer (according to your classification), 
> I need time to learn this new stuff and I don’t want to leave everything 
> behind that I have coded in my miserable days of untyped hacking. I have
> moved some to TR, and it interoperates nicely with R. So if you want me 
> to accept the supreme gift of AC’s TR2, you need to allow me to migrate
> in the same incremental manner — unless your goal is to leave all miserable 
> programmers, such as myself, behind. Nothing prevents you from that. Go
> create TR-leave-eveeryone-else-behind. 
> 
> Glad you like Stephen’s work. — Matthias
> 
> 
> 
> 
>> On Jan 19, 2017, at 9:30 AM, Anthony Carrico  wrote:
>> 
>> On 01/18/2017 08:57 PM, Matthias Felleisen wrote:
>>> 
>>> And how would components in #lang typed/racket interact with components in 
>>> #lang kinded/racket interact? 
>> 
>> If this wasn't Matthias, I'd say whoever posted this missed the whole
>> point of Racket. Since it is Matthias, I'll take this as an invitation
>> to rant.
>> 
>> At its core, what is racket? Racket is an operating system with Scheme
>> values, rather than C values, as its foreign function interface. So the
>> simple answer to the question is that Typed Racket 2 uses Scheme values
>> as its FFI, just like everyone else does. Does this suck? Yes, but for
>> many cases it is better than using C values.
>> Any other vision of the module system is an illusion, I realized this as
>> soon as I tried Fathertime after the Scheme Workshop 10-20 years ago.
>> 
>> What do contemporary programmers want? They want some kind of static
>> proof that their interfaces are good. Why are so many programmers
>> sniffing around Racket these past few months? Because they noticed
>> Turnstile, and they recognize that Racket is the state of the art in
>> metaprogramming. The window is currently open, something like Racket +
>> Haskell/Idris/Purescript/Agda will emerge. Programmers will bleed from
>> both camps.  Recognize this, or lose all good Racket programmers. Anyone
>> who uses typed Racket discovers Haskell, and start to hate Racket
>> because it doesn't have typeclasses. It feels like programming with your
>> arms chopped off. They don't want to give up Matthew's great work, so
>> they will bring it with them one way or another.
>> 
>> Typed Racket was a fine experiment. It accomplished two things. It
>> showed dynamic programmers that static types and other proofs should be
>> employed when possible, and contracts should be employed otherwise.
>> Typed Racket killed Scheme. This is speaking as one of the few
>> programmers in the world who has been paid to program in typed racket.
>> 
>> -- 
>> Anthony Carrico
>> 
>> -- 
>> You received this message because you are subscribed to the Google Groups 
>> "Racket Users" group.
>> To unsubscribe from this group and stop receiving emails from it, send an 
>> email to racket-users+unsubscr...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Matthias Felleisen]

You’re preaching to the choir. See Racket Manifesto. 

But you’re also preaching to the guy who got this project to
where it is because "Types Suck” has been my slogan for decades. 
(I will leave it to figure out what that slogan means.) 

Since I am not a good programmer (according to your classification), 
I need time to learn this new stuff and I don’t want to leave everything 
behind that I have coded in my miserable days of untyped hacking. I have
moved some to TR, and it interoperates nicely with R. So if you want me 
to accept the supreme gift of AC’s TR2, you need to allow me to migrate
in the same incremental manner — unless your goal is to leave all miserable 
programmers, such as myself, behind. Nothing prevents you from that. Go
create TR-leave-eveeryone-else-behind. 

Glad you like Stephen’s work. — Matthias




> On Jan 19, 2017, at 9:30 AM, Anthony Carrico  wrote:
> 
> On 01/18/2017 08:57 PM, Matthias Felleisen wrote:
>> 
>> And how would components in #lang typed/racket interact with components in 
>> #lang kinded/racket interact? 
> 
> If this wasn't Matthias, I'd say whoever posted this missed the whole
> point of Racket. Since it is Matthias, I'll take this as an invitation
> to rant.
> 
> At its core, what is racket? Racket is an operating system with Scheme
> values, rather than C values, as its foreign function interface. So the
> simple answer to the question is that Typed Racket 2 uses Scheme values
> as its FFI, just like everyone else does. Does this suck? Yes, but for
> many cases it is better than using C values.
> Any other vision of the module system is an illusion, I realized this as
> soon as I tried Fathertime after the Scheme Workshop 10-20 years ago.
> 
> What do contemporary programmers want? They want some kind of static
> proof that their interfaces are good. Why are so many programmers
> sniffing around Racket these past few months? Because they noticed
> Turnstile, and they recognize that Racket is the state of the art in
> metaprogramming. The window is currently open, something like Racket +
> Haskell/Idris/Purescript/Agda will emerge. Programmers will bleed from
> both camps.  Recognize this, or lose all good Racket programmers. Anyone
> who uses typed Racket discovers Haskell, and start to hate Racket
> because it doesn't have typeclasses. It feels like programming with your
> arms chopped off. They don't want to give up Matthew's great work, so
> they will bring it with them one way or another.
> 
> Typed Racket was a fine experiment. It accomplished two things. It
> showed dynamic programmers that static types and other proofs should be
> employed when possible, and contracts should be employed otherwise.
> Typed Racket killed Scheme. This is speaking as one of the few
> programmers in the world who has been paid to program in typed racket.
> 
> -- 
> Anthony Carrico
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Anthony Carrico]

On 01/19/2017 09:30 AM, Anthony Carrico wrote:
> What do contemporary programmers want? They want some kind of static
> proof that their interfaces are good.


I didn't put the following in my rant, because why muddy a good rant?
But to elaborate, they also want productivity, and that means
state-of-the-art polymorphism, and that also comes along with a good
type system.

-- 
Anthony Carrico

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Anthony Carrico]

On 01/19/2017 09:50 AM, Robert Kuzelj wrote:
> Wow! My question seems to be pretty  upstirring. ;-)
> But you are completely right - I am sniffing around Racket (Typed) bc strong 
> typing + meta programming look like a killer combo.
> 
> And btw. yeah something will emerge ... or rather has already emerged
> https://github.com/LuxLang/lux
> https://luxlang.gitbooks.io/the-lux-programming-language/content/

See also Alexis King's:
https://lexi-lambda.github.io/blog/2017/01/05/rascal-is-now-hackett-plus-some-answers-to-questions/

-- 
Anthony Carrico

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Robert Kuzelj]

Wow! My question seems to be pretty  upstirring. ;-)
But you are completely right - I am sniffing around Racket (Typed) bc strong 
typing + meta programming look like a killer combo.

And btw. yeah something will emerge ... or rather has already emerged
https://github.com/LuxLang/lux
https://luxlang.gitbooks.io/the-lux-programming-language/content/

Nevertheless I think Racket having somehow the bigger organisation/resources 
could be leading here

Am Donnerstag, 19. Januar 2017 15:31:01 UTC+1 schrieb Anthony Carrico:
> On 01/18/2017 08:57 PM, Matthias Felleisen wrote:
> > 
> > And how would components in #lang typed/racket interact with components in 
> > #lang kinded/racket interact? 
> 
> If this wasn't Matthias, I'd say whoever posted this missed the whole
> point of Racket. Since it is Matthias, I'll take this as an invitation
> to rant.
> 
> At its core, what is racket? Racket is an operating system with Scheme
> values, rather than C values, as its foreign function interface. So the
> simple answer to the question is that Typed Racket 2 uses Scheme values
> as its FFI, just like everyone else does. Does this suck? Yes, but for
> many cases it is better than using C values.
> Any other vision of the module system is an illusion, I realized this as
> soon as I tried Fathertime after the Scheme Workshop 10-20 years ago.
> 
> What do contemporary programmers want? They want some kind of static
> proof that their interfaces are good. Why are so many programmers
> sniffing around Racket these past few months? Because they noticed
> Turnstile, and they recognize that Racket is the state of the art in
> metaprogramming. The window is currently open, something like Racket +
> Haskell/Idris/Purescript/Agda will emerge. Programmers will bleed from
> both camps.  Recognize this, or lose all good Racket programmers. Anyone
> who uses typed Racket discovers Haskell, and start to hate Racket
> because it doesn't have typeclasses. It feels like programming with your
> arms chopped off. They don't want to give up Matthew's great work, so
> they will bring it with them one way or another.
> 
> Typed Racket was a fine experiment. It accomplished two things. It
> showed dynamic programmers that static types and other proofs should be
> employed when possible, and contracts should be employed otherwise.
> Typed Racket killed Scheme. This is speaking as one of the few
> programmers in the world who has been paid to program in typed racket.
> 
> -- 
> Anthony Carrico

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Anthony Carrico]

On 01/18/2017 08:57 PM, Matthias Felleisen wrote:
> 
> And how would components in #lang typed/racket interact with components in 
> #lang kinded/racket interact? 

If this wasn't Matthias, I'd say whoever posted this missed the whole
point of Racket. Since it is Matthias, I'll take this as an invitation
to rant.

At its core, what is racket? Racket is an operating system with Scheme
values, rather than C values, as its foreign function interface. So the
simple answer to the question is that Typed Racket 2 uses Scheme values
as its FFI, just like everyone else does. Does this suck? Yes, but for
many cases it is better than using C values.
Any other vision of the module system is an illusion, I realized this as
soon as I tried Fathertime after the Scheme Workshop 10-20 years ago.

What do contemporary programmers want? They want some kind of static
proof that their interfaces are good. Why are so many programmers
sniffing around Racket these past few months? Because they noticed
Turnstile, and they recognize that Racket is the state of the art in
metaprogramming. The window is currently open, something like Racket +
Haskell/Idris/Purescript/Agda will emerge. Programmers will bleed from
both camps.  Recognize this, or lose all good Racket programmers. Anyone
who uses typed Racket discovers Haskell, and start to hate Racket
because it doesn't have typeclasses. It feels like programming with your
arms chopped off. They don't want to give up Matthew's great work, so
they will bring it with them one way or another.

Typed Racket was a fine experiment. It accomplished two things. It
showed dynamic programmers that static types and other proofs should be
employed when possible, and contracts should be employed otherwise.
Typed Racket killed Scheme. This is speaking as one of the few
programmers in the world who has been paid to program in typed racket.

-- 
Anthony Carrico

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Robert Kuzelj]

> And how would components in #lang typed/racket interact with components in 
> #lang kinded/racket interact? 

maybe (if there is no other way) not at all and there would a breaking of 
compatibility?!

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Matthias Felleisen]

And how would components in #lang typed/racket interact with components in 
#lang kinded/racket interact? 


> On Jan 18, 2017, at 8:16 PM, Anthony Carrico  wrote:
> 
> On 01/17/2017 05:31 AM, Sam Tobin-Hochstadt wrote:
>> The major obstacle is that the current kind system design is not easy to
>> reconcile with higher kinds. This is mostly because the current system
>> is poorly designed, but we need to avoid breaking existing programs.
> 
> Why is this an issue? #lang something/else, and the problem is solved, no?
> 
> -- 
> Anthony Carrico
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Anthony Carrico]

On 01/17/2017 05:31 AM, Sam Tobin-Hochstadt wrote:
> The major obstacle is that the current kind system design is not easy to
> reconcile with higher kinds. This is mostly because the current system
> is poorly designed, but we need to avoid breaking existing programs.

Why is this an issue? #lang something/else, and the problem is solved, no?

-- 
Anthony Carrico

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Sam Tobin-Hochstadt]

The major obstacle is that the current kind system design is not easy to
reconcile with higher kinds. This is mostly because the current system is
poorly designed, but we need to avoid breaking existing programs.

Sam

On Tue, Jan 17, 2017, 11:19 AM Robert Kuzelj  wrote:

> Am Dienstag, 17. Januar 2017 10:34:54 UTC+1 schrieb Sam Tobin-Hochstadt:
> > No, unfortunately  you can't just higher kinds in Typed Racket. This is
> a limitation we hope to lift eventually, though.
>
> Hi Sam,
>
> Thanks for the fast answer.
> Is there any specific obstacles that are in the way of implementing it?
> Assuming that HKT are generally well understood (so it seems to me).
>
> Best regards
>
> Robert
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Robert Kuzelj]

Am Dienstag, 17. Januar 2017 10:34:54 UTC+1 schrieb Sam Tobin-Hochstadt:
> No, unfortunately  you can't just higher kinds in Typed Racket. This is a 
> limitation we hope to lift eventually, though.

Hi Sam,

Thanks for the fast answer.
Is there any specific obstacles that are in the way of implementing it? 
Assuming that HKT are generally well understood (so it seems to me).

Best regards

Robert 

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Typed Racket & Higher Kinded Types

[Sam Tobin-Hochstadt]

No, unfortunately  you can't just higher kinds in Typed Racket. This is a
limitation we hope to lift eventually, though.

Sam

On Tue, Jan 17, 2017, 10:29 AM Robert Kuzelj  wrote:

> Hi,
>
> does Typed/Racket support higher kinded types? I couldn't find any infos
> on the docs in regards to that.
>
> Thx
>
> Best regards
>
> Robert
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[racket-users] Typed Racket & Higher Kinded Types

[Robert Kuzelj]

Hi,

does Typed/Racket support higher kinded types? I couldn't find any infos on the 
docs in regards to that.

Thx

Best regards

Robert

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.