executor, mostly

notes/type_system/definitions.md

@@ -1,11 +1,20 @@
 ## Type definitions
 
+A new type can be created with the define expression, which associates a templated expression of
+type `type` with a name and a template. The name allocated in this fashion is always representedas
+an Atom of type `type` or some function that eventually returns `type`. The kind of the template
+parameters is always inferred to be `type` rather than deduced from context.
+
+The following type definition
+
 ```orc
-define Cons as \T:type. loop \r. Option (Pair T r)
+define Cons $T as loop \r. Option (Pair $T r)
 ```
 
-Results in
-- (Cons Int) is not assignable to @T. Option T
+results in these conditions:
+
+- (Cons Int) is not assignable to @T. Option T, or any other type expression that its
+  definitions would be assignable to, and vice versa.
 - An instance of (Cons Int) can be constructed with `categorise @(Cons Int) (some (pair 1 none))`
   but the type parameter can also be inferred from the expected return type
 - An instance of (Cons Int) can be deconstructed with `generalise @(Cons Int) numbers`
@@ -28,8 +37,18 @@ The following must unify:
 Mult Int (Cons Int) (Cons Int)
 ```
 
-### Impls for types
+## Typeclasses
 
-Impls for types are generally not a good idea as autos with types like Int can
-often be used in dependent typing to represent eg. an index into a type-level conslist to be
-deduced by the compiler, and impls take precedence over resolution by unification.
+Typeclasses and types use the same define syntax. In fact, much like a type is nothing but a
+distinguished instance of the underlying type with added meaning and constraints, a typeclass is
+nothing but a distinguished instance of the underlying function (or collection of functions) with
+added meaning and constraints. A typeclass definition is therefore perfectly identical to a type
+definition:
+
+```
+define Add $T $U $R as $T -> $U -> $R
+```
+
+It is clear that the definition of this type would match many, many functions, including
+multiplication, so functions that should be considered addition are [impls](./impls.md) of the
+typeclass Add.

notes/type_system/impls.md

@@ -11,6 +11,12 @@ An impl candidate can be used to resolve an auto if
 - it is not present in any other matching impl's override tree
 - all other candidates are present in its override tree
 
+### Impls for types
+
+Impls for types are generally not a good idea as autos with types like Int can
+often be used in dependent typing to represent eg. an index into a type-level conslist to be
+deduced by the compiler, and impls take precedence over resolution by unification.
+
 In Rust impls can be placed in one of two modules; the trait owner, and the type owner. In orchid
 that is not the case, so two additional possibilities arise that Rust's orphan rules prevent.