Typed Racket & Higher Kinded Types

262 views
Skip to first unread message

Robert Kuzelj

unread,
Jan 17, 2017, 4:29:03 AM1/17/17
to Racket Users
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

Sam Tobin-Hochstadt

unread,
Jan 17, 2017, 4:34:54 AM1/17/17
to Robert Kuzelj, Racket Users

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

Sam


--
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...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Robert Kuzelj

unread,
Jan 17, 2017, 5:19:53 AM1/17/17
to Racket Users, rob...@robkuz.com, sa...@cs.indiana.edu
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

Sam Tobin-Hochstadt

unread,
Jan 17, 2017, 5:31:51 AM1/17/17
to Robert Kuzelj, Racket Users
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

Robert Kuzelj

unread,
Jan 17, 2017, 5:47:43 AM1/17/17
to Racket Users, rob...@robkuz.com, sa...@cs.indiana.edu

> 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.

hmm, that doesn't sound as there will be any changes to that any time soon. <sigh>

Anthony Carrico

unread,
Jan 18, 2017, 8:16:35 PM1/18/17
to racket...@googlegroups.com
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

Matthias Felleisen

unread,
Jan 18, 2017, 8:57:50 PM1/18/17
to Anthony Carrico, racket...@googlegroups.com

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

Robert Kuzelj

unread,
Jan 19, 2017, 4:44:01 AM1/19/17
to Racket Users, acar...@memebeam.org, matt...@ccs.neu.edu
> 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?!

Anthony Carrico

unread,
Jan 19, 2017, 9:31:01 AM1/19/17
to racket...@googlegroups.com
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

Robert Kuzelj

unread,
Jan 19, 2017, 9:50:28 AM1/19/17
to Racket Users
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

Anthony Carrico

unread,
Jan 19, 2017, 9:56:21 AM1/19/17
to racket...@googlegroups.com
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

Anthony Carrico

unread,
Jan 19, 2017, 10:02:50 AM1/19/17
to racket...@googlegroups.com
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

Matthias Felleisen

unread,
Jan 19, 2017, 10:57:37 AM1/19/17
to Anthony Carrico, racket...@googlegroups.com

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

Matthias Felleisen

unread,
Jan 19, 2017, 11:17:18 AM1/19/17
to Anthony Carrico, racket...@googlegroups.com

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.

Robert Kuzelj

unread,
Jan 19, 2017, 11:42:17 AM1/19/17
to Racket Users, acar...@memebeam.org, matt...@ccs.neu.edu
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#.

Vincent St-Amour

unread,
Jan 19, 2017, 3:22:44 PM1/19/17
to Robert Kuzelj, Racket Users, acar...@memebeam.org, matt...@ccs.neu.edu
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

Anthony Carrico

unread,
Jan 20, 2017, 12:11:08 PM1/20/17
to Sam Tobin-Hochstadt, Robert Kuzelj, Racket Users
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

Reply all
Reply to author
Forward
0 new messages