doc: update docs

Author: cstml

docs/compiler.md

@@ -1,57 +1,55 @@
-# Compiler Spec & Design
+# _Compiler_ Spec & Design
 
-The Compiler component sits between the Frontend component and the Codegen
-component. The purpose of this component is to typecheck (or, more accurately,
-kindcheck) the Frontend's output (_Compiler Input_) and perform other additional
-validation checks necessary to ensure that the Codegen component is capable of
-processing the _Compiler Output_.
+The _Compiler_ component sits between the _Frontend_ component and the code
+generation component named _Codegen_. The purpose of the _Compiler_ is to
+typecheck terms generated by the Frontend (terms referred to as _Compiler Input_)
+and perform other additional validation checks. The end goal of the _Compiler_
+is to ensure that the _Codegen_ component is capable of processing the _Compiler
+Output_.
 
-## Compiler interface
+## _Compiler_ interface
 
-The Compiler operates on the Compiler Input proto, effectively enabling any
-number of Frontends to interface with the Compiler in a language agnostic
-manner.
+The _Compiler_ operates on the _Compiler Input proto_ - enabling, any _Frontend_
+to interface with the _Compiler_ in a language agnostic manner.
 
-Similarly, the Compiler Output is also a proto that is then consumed by Codegen
-modules that can be written in any programming environment capable of
-communicating using Google Protobufs.
+Similarly, the _Compiler Output_ is also a _proto_ that is then consumed by
+_Codegen_ modules, able to be written in any programming environment capable of
+communicating via Google Protocol Buffers.
 
 ## Checking type definitions
 
-One primary purpose of the compiler is to typecheck the schemata that users
-define via the Frontend. The lambda calculus representation of schemata is "one
-level up" from the term level: ADT schemata declarations are the "terms" and
-kinds are the "types".
-
-Because the schema language only supports data declarations for algebraic data
-types, and does not support function definitions, the only two admissible kinds
-are `Type` and `TyCon`s of a specific arity, such that a `TyCon` can accept an
-arbitrary number of arguments of kind `Type` but can **only** accept arguments
-of kind `Type`. Put another way: An expression's kind is the same thing as its
-arity, and only expressions of arity=0 (i.e. expressions of kind `Type`) can be
-applied.
-
-To elaborate on the previous point: A user can define a higher kinded data type,
-such as `data Maybe a = Nothing | Just a` in the schema language. However users
-cannot define a data type which has a higher kinded type as a _parameter_, and
-users must "fully saturate" higher kinded types with well-scoped type variables
-or zero arity `Type`s to pass them as arguments to a `TyCon`. Consequently, a
-definition such as `data HKT f a = HKT (f a)` is not valid because `f :: Type ->
-Type`. Restricting the schema language in this way does reduce its
-expressiveness, but allowing higher kinded type parameters would greatly limit
-(or, at the very least, greatly complicate) our ability to codegen for a variety
-of target languages with type systems less expressive than Haskell.
-
-The schema language supports recursive types, and so the compiler must be
-capable of checking recursive types.
-
-In addition to typechecking, the compiler must perform a special check for
+The primary purpose of the compiler is to typecheck the schemata that users
+define via the _Frontend_. The schemata terms are ADT declarations and their
+types are kinds.
+
+Currently the schema language supports:
+
+ 1. types (such as `Int` or `Bool`),
+
+ 2. and type functions (such as `Maybe` or `Either`).
+
+There are future plans to expand this to Higher Kinded Types (such as `MaybeT`,
+`StateT` etc.) - subject to research into _Codegen_ of such types in the target
+languages. The schema language and the _Compiler_ do support recursive
+types.
+
+Schemata terms must be monomorphically kinded, with polymorphic kinds defaulting
+to monomorphic ones. For example `Phantom a = Phantom` would resolve to the
+monomorphic kind `Type → Type` rather than the polymorphic kind `∀a. a → Type`.
+
+<!-- cstml comments: Is this true? I think it's an Aim not a requirement?
+:todo: -->
+
+In addition to typechecking, the compiler must  perform a special check for
 recursive types: It must validate that a recursive type is inhabited (or
 inhabitable). The purpose of this check is to ensure that any schema which
 passes validation is (in principle) a schema for which type definitions and
 typeclass "instances" (which may be simple functions in languages without
 typeclass support) can be generated. As an example, the compiler should reject
-types such as `data F a = F (F a)`, which is uninhabited (and uninhabitable).
+types such as `data F a = F (F a)`, which is uninhabited.
+
+<!-- cstml comments: Is this true? Seems as though this should fail
+parsing. :todo: -->
 
 (Provisional:) Finally, the compiler should _normalize_ expressions as far as it
 is able to. For example, it may be possible to define a data type in the schema
@@ -62,12 +60,12 @@ generation.
 
 ## Checking type class definitions and instance clauses
 
-The Compiler should, if possible, ensure that all instance declarations for
+The _Compiler_ should, if possible, ensure that all instance declarations for
 schemata are derivable using hard-coded derivation axioms. Because the checks
 relevant to validating type class instances ough to be entirely separate from
 the checks enumerated above, they can be worked on separately at a later date
 when the design of the typeclass system has been fleshed out more.
 
 ## Unsolved Problems
 
-- How do we represent recursive types in our lambda calculus AST?
+- [ ] How do we represent recursive types in our lambda calculus AST?