Kinds are Calling Conventions
summary
An intermediate language encodes runtime representation, arity and evaluation strategy inside kinds so multi-argument calls compile statically even under polymorphism. It adds a TYPE r c kind for representation and calling convention, a distinct primitive squiggly arrow function type with unrestricted eta but controlled beta, and explicit closures via Clos and App so partial applications share work. A compiler pipeline and metatheory prove well-kinded programs always lower to an efficient calling convention.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:15Efficient Function Calls
- 1:32Determining Function Arity
- 3:01What Is Arity?
- 5:25Static Arity
- 6:30Currying
- 8:07Functions are Called
- 9:42The Problem With Polymorphism
- 11:14Arity Polymorphism
- 13:46Even More
related talks
43mAdding kind-polymorphism to the Scala programming language
46mAdding kind-polymorphism to the Scala programming language
41mThe Dialectics of Type-Level Programming
18mA Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…
01h 03mMatching Logic: Foundation of the K Framework
31mProgramming Languages Must Have Formal Semantics. Period.
19mIll-Typed Programs Don't Evaluate
24mAll for one and none forall: Compiling polymorphic relations without(…)