Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

wu0014: Add more details about type system #20

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

wu0014: Add more details about type system #20

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
116 changes: 74 additions & 42 deletions docs/writeups/0014-type-system.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,9 +44,53 @@ We will say that `Point[T]` has kind `type -> type`.
Even more complicated: `jinko`'s module system creates a new `type` out of the path of a module, encoded as a string. Out of a `string`, create a new `type`. This has kind `string -> type`.
If we imagine a "thing" which requires an integer and a type to return a new type, then that "thing" would be of kind `(int, type) -> type`.

## Sets

In `jinko`, types can all be represented as sets. According to wikipedia, sets are ["the mathematical model for a collection of different things"](https://en.wikipedia.org/wiki/Set_(mathematics)), so we will call the components of our sets "things".

Thus, in `jinko`, a type is a `Set` of `Thing`s. The notation we will use in the examples is as follows:

1. Each `Thing` will be written as its name: `int`, `Complex`, `float`
2. Each type will be represented as the set of its things using curly brackets: `{ int, string }`

```rust
where x /* { int } */ = 15;

where y: string | int /* { string, int } */ =
if condition() { x } else { "none" }
```

We can add a number of rules around sets and things:

1. The type of a binding is always a `Set`, even if it contains only one `Thing`

```rust
where x = 196.4; // { float }

func foo(
a: int, // { int }
b: bool, // { bool }
) -> char // { char }
{
'a' // { char }
} // { func({int}, {bool}) -> {char} }
```

2. `switch` expressions are the only ones allowed to explore the `Thing`s within a `Set`

```rust
where x = int | string | char = '1'; // { int, string, char }

switch x {
i: int -> handle_int(i /* { int } */),
s: string -> handle_string(s /* { string } */),
c: char -> handle_char(c /* { char } */),
}
```

## Creating types

With this knowledge in mind, `jinko`'s type system can be thought of as an interpreter which only deals with kinds and which has no side-effects. All of the execution and logic happens during type-checking.
With this knowledge in mind, `jinko`'s type system can be thought of as an interpreter which only deals with kinds and which has no side-effects. Its goal is to ensure that different `Set`s are compatible with each other, otherwise it will output an error. All of the execution and logic happens during type-checking.
In that system, a concrete type of kind `type` can be thought of as a regular immutable variable/binding. A type constructor of kind `type -> type` can be thought of as a regular function.

In the following code examples, comments will be added around the various types to show the kinds we are dealing with:
Expand All @@ -57,6 +101,20 @@ type Foo; // :: type
type Foo[T]; // :: type -> type
```

Which we can combine with `Set` information

```rust
type Foo; // :: type { Foo }

type Foo[T]; // :: type -> type
```

You can note that type constructors *are not `Set`s*. Meaning that the typechecker will not perform any checking on type constructors, but only on types of kind `type`. Meaning that generic types and generic functions must be monomorphized fully for the typechecker to reason about them.

To apply one of the points above, the first `Foo` type is similar to a binding, while the second one can be though of as a "function" which will produce a binding when called (monormorphized).

## Two types of types

There are two different types in `jinko`: sum types and record types. Sum types are made of multiple possible types but instances of a sum type are only ever *one* type. Record types on the other hand, are a product type: they contain multiple instances of possibly multiple types.

```rust
Expand All @@ -70,17 +128,17 @@ In the above example, `Foo` is a record type with no data fields. `Bar` is a rec
func foo(a: int | bool | char) {}
```

Here on the other hand, the argument `a` is of the sum type `int | bool | char`. `a` will be either an integer, a boolean or a character. Let's add the kinds to these two examples:
Here on the other hand, the argument `a` is of the sum type `int | bool | char`. `a` will be either an integer, a boolean or a character. Let's add extra info to these examples:

```rust
type Foo; // :: type
type Foo; // :: type { Foo }
type Bar(
a: int, // :: type
b: Foo, // :: type
); // :: type
a: int, // :: type { int }
b: Foo, // :: type { Foo }
); // :: type { Bar }

func foo(
a: int | bool | char // :: type
a: int | bool | char // type { int, bool, char }
) {}
```

Expand All @@ -93,53 +151,27 @@ type Bar = Foo; // :: type

This is similar to creating two "variables" in a regular piece of code. One is named `Foo`, and the other, `Bar`, refers to `Foo`. `Bar` is a type alias of `Foo` - not a new type. Anywhere `Foo` is used, `Bar` could be used, and vice-versa.

Another concept we introduce in the above example is that function arguments can be typed with values of kind `type`. It is not possible for a function argument to be of kind `type -> type`, or other type constructors. This is an important concept, as one could think tihs is not the case with the following example:
Another concept we introduce in the above example is that function arguments can be typed with values of kind `type`. It is not possible for a function argument to be of kind `type -> type`, or other type constructors. This is an important concept, as one could think this is not the case with the following example:

```rust
func foo[T](value: Maybe[T]) {}
```

However, this function is only valid when fully monomorphized - meaning that `value` will only ever accept a type of kind `type`.
However, as we said above, the typechecker can only reason about this function when fully monomorphized - meaning that `value` will only ever accept a type of kind `type`. At the moment, `foo` is a function constructor.

## Sets

In `jinko`, types can all be represented as sets. According to wikipedia, sets are ["the mathematical model for a collection of different things"](https://en.wikipedia.org/wiki/Set_(mathematics)), so we will call the components of our sets "things".

Thus, in `jinko`, a type is a `Set` of `Thing`s. The notation we will use in the examples is as follows:

1. Each `Thing` will be written as its name: `int`, `Complex`, `float`
2. Each type will be represented as the set of its things using curly brackets: `{ int, string }`
Furthermore, we can also alias sum types:

```rust
where x /* { int } */ = 15;

where y: string | int /* { string, int } */ =
if condition() { x } else { "none" }
type FooOrBar = Foo | Bar; // :: type { Foo, Bar }
```

We can add a number of rules around sets and things:

1. The type of a binding is always a `Set`, even if it contains only one `Thing`
And store sum types in record types:

```rust
where x = 196.4; // { float }
type Record(
i_or_s: int | string // :: type { int, string }
); // :: type { Record }

func foo(
a: int, /* { int } */
b: bool, /* { bool } */
) -> char /* { char } */ {
'a' /* { char } */
} /* { func({int}, {bool}) -> {char} } */
```

2. `switch` expressions are the only ones allowed to explore the `Thing`s within a `Set`

```rust
where x = int | string | char = '1'; // { int, string, char }

switch x {
i: int -> handle_int(i /* { int } */),
s: string -> handle_string(s /* { string } */),
c: char -> handle_char(c /* { char } */),
}
```
Let's pause here and have a look at one of the major differences between record types and sum types. You'll note that the `Set` of `Record` is `{ Record }`. It does not matter that `Record` has a field with a type of `int | string`. We cannot "implicitly" convert a value of type `int | string` into a value of type `Record`. On the other hand, `FooOrBar` has type `Foo | Bar`.