de-lambda-ified function types are cool. i should write up a blog post about the idea
-
Show this thread
-
Replying to @beka_valentine @psygnisfive
Are these supercombinators? https://wiki.haskell.org/Super_combinator …
1 reply 0 retweets 2 likes -
Replying to @asajeffrey
no, but they're related! supercombinators are just lambdas w/ no free vars (ie non-closures), but this idea is like giving those things primitive *names* in the type theory and abolishing lambdas entirely!
1 reply 0 retweets 2 likes -
Replying to @beka_valentine @psygnisfive
Ah, that's cool. When they're used in a compiler, supercombinators are usually named, because those names are used as labels in codegen. But I can imagine those names would be useful in a type system, e.g. for dependent types.
1 reply 0 retweets 2 likes -
Replying to @asajeffrey
basically the idea here is to give a concrete type theory for the thing that you'd like to do for compilation. its a type theory for supercombinators as primitive notions of function :)
1 reply 0 retweets 1 like -
Replying to @beka_valentine @psygnisfive
I wonder if
@edwinbrady has about thoughts about this, since Idris uses the Epic supercombinators back end.1 reply 0 retweets 2 likes -
Replying to @asajeffrey @psygnisfive
These days Idris defunctionalises rather than using Epic. Though I could imagine this idea helping with compile-time evaluation…
2 replies 0 retweets 1 like
In particular, I want this: https://xavierleroy.org/publi/strong-reduction.pdf … - it’s a lot of work to implement though. Maybe this idea will help…
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.