Type Annotations

[evincarofautumn]

Type annotations serve as documentation, and as a sanity check to prevent weird types being inferred for miswritten recursive and higher-order functions. The preliminary syntax for annotations is like so:

type (a b) map: {a -> b} [a] -> [b]
type succ { int -> int }

Or more generally:

type (VARS) NAME { TYPE }

Where all variables used in TYPE must be quantified by VARS, and TYPE has the following syntax:

Type	Meaning
a	Value of type a
a0 a1 … -> b0 b1 …	Function consuming a and producing b
[a]	Vector with elements of type a
(a b …)	Tuple with elements of type a, b, &c
{ … }	Grouping
bool int text	Intrinsic types

[evincarofautumn]

Basically feature-complete, but not thoroughly tested, and definitely in need of cleanup.

Currently, function signatures must quantify all “rest of the stack” variables. This is a UX issue for constants:

def pi_ish 3

-- Want:
type pi_ish int

-- Have:
type (A) pi_ish: A -> A int

And also for higher-order functions:

-- Want:
type (a) downtop: [a] {[a] -> [a]} {a -> a} -> [a]

-- Have:
type (A B C a) downtop: A [a] {B [a] -> B [a]} {C a -> C a} -> A [a]

I intend to eliminate the need for stack variables unless they are actually used, requiring an explicit ... suffix otherwise to indicate stack-kindedness:

type (A B C a) downtop:
  A... [a] {B... [a] -> B... [a]} {C... a -> C... a} -> A... [a]

It is not possible to give type signatures to arbitrary terms, only user definitions. I don’t intend to go beyond this yet. “It could be nice”, though tempting, is not a good enough reason.

type (A B) apply: A... {A... -> B...} -> B...

[kputnam]

I have the same predicament about wanting to elide "rest of the stack" variables and the ability to ascribe types to arbitrary expressions.

One alternate take on your syntax is moving the "kind declaration" into the parameter list, like this: type (A... B...): A { A -> B } -> B. I'm curious to get your take on inferring missing stack variables. The pi_ish example makes me think there could be some ambiguity: clearly int means S -> S int but does dup :: a -> a a mean S a -> S a a or S -> S (T a -> T a a)? To rephrase, should you always infer both a fresh stack variable and an arrow type like pi_ish, or should you only infer the arrow if one wasn't already present like dup?

[evincarofautumn]

I’ve been mulling over this whole thing for a few days. I’ve come to the conclusion that wherever you have an inferred function type, you can immediately generalise it over the rest of the stack. Every function is polymorphic with respect to the part of the stack on which it has no effect, so it’s sensible and sound to encode this. I just haven’t gotten round to implementing it yet. Builtins do not work this way—particularly apply :: ∀A B. A (A → B) → B—but of course those are treated somewhat specially anyhow.

I don’t actually think it’s a good idea to infer “missing” stack variables per se. That would imply an implicit conversion from base types a to universally quantified polymorphic function types ∀A. A → A a. Simply put, I think -> int is an acceptable type for pi_ish. :)

[evincarofautumn]

Absorbed by the rewrite.