A type system for haku #110

New issue

Open

opened 2024-10-28 21:40:01 +01:00 by riki · 3 comments

riki commented

2024-10-28 21:40:01 +01:00

Owner

A type system would allow us to have more clear error messages, as well as make the language easier to analyse for IDE-style features.

This type system would not be visible to outside users, but rather use full program type inference to point out mistakes ahead of time without you having to annotate anything.

-- addVectors : \vec, vec -> vec
addVectors = \a, b ->
  -- vecX : \vec -> number
  --   => therefore a must be a vec
  --   => therefore b must be a vec
  vec (vecX a + vecX b) (vecY a + vecY b)

I've never written a type system with constraint-based type inference like this before, so it will probably require a lot of research work to be pulled off. I also worry the error messages may end up not being clear enough for users to understand, but we'll see how that goes.

A type system would allow us to have more clear error messages, as well as make the language easier to analyse for IDE-style features. This type system would not be visible to outside users, but rather use full program type inference to point out mistakes ahead of time without you having to annotate anything. ``` -- addVectors : \vec, vec -> vec addVectors = \a, b -> -- vecX : \vec -> number -- => therefore a must be a vec -- => therefore b must be a vec vec (vecX a + vecX b) (vecY a + vecY b) ``` I've never written a type system with constraint-based type inference like this before, so it will probably require a lot of research work to be pulled off. I also worry the error messages may end up not being clear enough for users to understand, but we'll see how that goes.

riki added the

area/haku

label 2024-10-28 21:40:01 +01:00

riki referenced this issue

2025-06-30 15:01:02 +02:00

haku, version 2 #121

riki commented

2025-07-01 10:56:40 +02:00

Author

Owner

A taxonomy of types in haku:

[] - Nothing
boolean - Represented using the special tags True and False
number - 32-bit float
Tag - Literally just the tag Tag. Each tag is its own type.
n t - Static list of n x t elements. Result of [] literals. 2 number, 3 number, 4 number replace vec and rgba
list t - Dynamic list of any number of t elements
\a -> r - Function accepting the argument a and returning the value r. There can be more than one argument, but there's always at least one. If that argument is irrelevant, the type is \[] -> t.
{ A = t } - Record. Acts like a function which can be called with A as its argument to get a value of type t.
act - An action the brush can take. A reticle, scribble, or a list containing any amount of scribbles.
- reticle - A latent input from the user—such as the dotter, the selectRect, or the editRect.
- scribble - An output from the brush—such as the stroke or fill.
shape - A shape that can be scribbled.
- line - A line segment.
- rect - An axis-aligned rectangle.
- circle - A circle with a position and radius.

Subtyping relationships:

[] <: list t   -- list of 0 elements
n t <: list t  -- list of n elements

reticle <: act
scribble <: act
list scribble <: scribble

2 number <: shape  -- point
line <: shape
rect <: shape
circle <: shape

A taxonomy of types in haku: - `[]` - Nothing - `boolean` - Represented using the special tags `True` and `False` - `number` - 32-bit float - `Tag` - Literally just the tag `Tag`. Each tag is its own type. - `n t` - Static list of `n` x `t` elements. Result of `[]` literals. `2 number`, `3 number`, `4 number` replace `vec` and `rgba` - `list t` - Dynamic list of any number of `t` elements - `\a -> r` - Function accepting the argument `a` and returning the value `r`. There can be more than one argument, but there's always at least one. If that argument is irrelevant, the type is `\[] -> t`. - `{ A = t }` - Record. Acts like a function which can be called with `A` as its argument to get a value of type `t`. - `act` - An action the brush can take. A reticle, scribble, or a list containing any amount of scribbles. - `reticle` - A latent input from the user—such as the `dotter`, the `selectRect`, or the `editRect`. - `scribble` - An output from the brush—such as the `stroke` or `fill`. - `shape` - A shape that can be scribbled. - `line` - A line segment. - `rect` - An axis-aligned rectangle. - `circle` - A circle with a position and radius. Subtyping relationships: ``` [] <: list t -- list of 0 elements n t <: list t -- list of n elements reticle <: act scribble <: act list scribble <: scribble 2 number <: shape -- point line <: shape rect <: shape circle <: shape ```

riki commented

2025-07-01 11:03:48 +02:00

Author

Owner

One extra typing rule that I'm not sure how to include here: I believe it should be possible to pass t wherever a function directly accepts n t, coercing it into a 1 t. This is so that we can make math functions like +, sin, etc. accept n number as an argument, and therefore work with arbitrarily-sized vectors and rgba.

Writing this rule down as t <: 1 t doesn't work, because it would result in infinite recursion—because if t <: 1 t, then also 1 t <: 1 (1 t), so on and so forth,

One extra typing rule that I'm not sure how to include here: I believe it should be possible to pass `t` wherever a function directly accepts `n t`, coercing it into a `1 t`. This is so that we can make math functions like `+`, `sin`, etc. accept `n number` as an argument, and therefore work with arbitrarily-sized vectors and `rgba`. Writing this rule down as `t <: 1 t` doesn't work, because it would result in infinite recursion—because if `t <: 1 t`, then also `1 t <: 1 (1 t)`, so on and so forth,

riki commented

2025-07-01 11:06:17 +02:00

Author

Owner

A note on n t: Indexing is still done via the index function, but elements 0–3 can be accessed alternatively by using function call syntax with the tags X, Y, Z, W, or R, G, B, and A. This also opens a path to swizzling in the future (but I don't want it in the MVP.)

Example: vec.X. This replaces the vecX vec and rgbaR set of functions.

A note on `n t`: Indexing is still done via the `index` function, but elements 0–3 can be accessed alternatively by using function call syntax with the tags `X`, `Y`, `Z`, `W`, or `R`, `G`, `B`, and `A`. This also opens a path to swizzling in the future (but I don't want it in the MVP.) Example: `vec.X`. This replaces the `vecX vec` and `rgbaR` set of functions.