Title cased everything

Author: bladyjoker

README.md

@@ -43,7 +43,11 @@ competitors if your project requires:
 
 ## Documentation
 
-- [Compiler](./docs/compiler.md)
+- [Design](./docs/design.md),
+- [Compiler](./docs/compiler.md),
+- [Codegen](./docs/codegen.md),
+- [Comparison matrix](./docs/comparison-matrix.md),
+- [User feedback](.docs/feedback)
 
 ## Getting started
 

docs/codegen.md

@@ -1,4 +1,4 @@
-# LambdaBuffers Codegen Spec & Design
+# LambdaBuffers Codegen
 
 NOTE: The implementation of the code generation framework is still in early stages and will likely undergo substantial changes as development continues. This document serves to outline general principles that any implementation of the LambdaBuffers code generation framework ought to adhere to.
 
@@ -9,23 +9,23 @@ NOTE: The implementation of the code generation framework is still in early stag
 3. Extensible to new opaque types
 4. Extensible to new type classes
 
-### Modular & reusable components
+### Modular & Reusable Components
 
 Because the code generation modules for each target language will almost certainly constitute the bulk of the final LambdaBuffers codebase, it is essential that components of the code generation framework be as modular and reusable as is practicable.
 
 Although each target language has its own distinct syntax and semantics, many syntactic forms exist in multiple target languages. For example, Haskell and PureScript both use a comma-separated set enclosed in square brackets (e.g. `[1,2,3]`) to represent a `List _/[_]` value, while Rust uses a similar form (in conjunction with a macro, e.g. `vec![1,2,3]`) to represent a `Vector<_>` value. To reduce redundant and superfluous code, common syntactic patterns such at this should be abstracted out into a set of functions that can be reused across languages.
 
-### Ergonomic interface
+### Ergonomic Interface
 
 While the LambdaBuffers team will support a finite set of specific target languages, adding support for an additional language should be as painless as possible (ceteris paribus) to encourage and facilitate open source contributions by third parties. A basic set of tools which can be used to write code generation modules for any target language should be developed, and all code generation modules written by the LambdaBuffers team should employ those tools (in order to provide a robust set of examples for future contributors, among other benefits).
 
-### Extensible to new opaque types
+### Extensible to New Opaque Types
 
 Users and contributors should be able to easily extend the default set of supported opaque types to support additional opaque types. In the context of code generation, this means: Users should have the ability to specify the target type for a given opaque type in the target language (including the package or module that contains the target type if the target type is not part of the language's standard library).
 
 Because type class instances must be derived structurally, and because an opaque type is by definition a type with no visible internal structure, users should be provided with an ergonomic interface for noting the presence of a type class instance for an opaque type's target type in a particular language (if the instance exists in the standard library), or for referring to the module where such an instance is located (if the instance is defined in a library or by the user in one of their own modules).
 
-### Extensible to new type classes
+### Extensible to New Type Classes
 
 Users and contributors should be able to easily extend the default set of supported type classes to support additional type classes and facilitate the derivation of instances for newly defined classes.
 

docs/command-line-interface.md

@@ -1,4 +1,4 @@
-# LambdaBuffers command line interface
+# LambdaBuffers Command Line Interface
 
 LambdaBuffers consists of three runtime command line interface components:
 

docs/comparison-matrix.md

@@ -11,12 +11,12 @@ Legend:
 - ❔ Not clear
 
 | **Feature**                                            | **Proto Buffers** | **ADL**      | **JSON Schema** | **Lambda Buffers** | **CDDL** | **ASN.1**    |
-|--------------------------------------------------------|-------------------|--------------|-----------------|--------------------|----------|--------------|
-| Sum Types                                              | 🟢                | 🟢           | 🔴              | 🟢                 | 🟢       | 🟢           |
-| Record Types                                           | 🟢                | 🟢           | 🟢              | 🟢                 | 🟢       | 🟢           |
-| Product Types                                          | 🔴                | 🔴           | 🔴              | 🟢                 | ❔       | 🔴           |
-| Recursive Types                                        | 🟢                | 🟢           | 🔴              | 🟢                 | 🟢       | ❔           |
-| Type functions (Generics)                              | 🔴                | 🟢           | 🔴              | 🟢                 | 🟢       | 🔴           |
+|--------------------------------------------------------+-------------------+--------------+-----------------+--------------------+----------+--------------|
+| Sum types                                              | 🟢                | 🟢           | 🔴              | 🟢                 | 🟢       | 🟢           |
+| Record types                                           | 🟢                | 🟢           | 🟢              | 🟢                 | 🟢       | 🟢           |
+| Product types                                          | 🔴                | 🔴           | 🔴              | 🟢                 | ❔       | 🔴           |
+| Recursive types                                        | 🟢                | 🟢           | 🔴              | 🟢                 | 🟢       | ❔           |
+| Parameterized types (generic types)                    | 🔴                | 🟢           | 🔴              | 🟢                 | 🟢       | 🔴           |
 | Type annotations/constraints                           | 🟢                | 🟢           | 🟢              | 🔵                 | 🟢       | 🟢           |
 | Add new builtin types                                  | 🔴                | 🟢           | 🔴              | 🟢                 | 🔴       | 🔴           |
 | Add new type semantics (e.g. different encodings)      | 🟢                | 🟢           | 🔴              | 🟢                 | 🔴       | 🟢           |
@@ -31,7 +31,38 @@ Legend:
 | Language specification                                 | 🟢                | 🟢           | 🟢              | 🟢                 | 🟢       | 🟢           |
 | Backwards compatibility strategy                       | 🟢                | 🔴           | 🔴              | 🔴                 | 🔴       | 🔴           |
 
-:todo: add chapter elaborating on each feature
+## Features
+
+### Sum types
+
+A type that can take on several different forms, also referred to as a *tagged
+union* or a *variant* (see https://en.wikipedia.org/wiki/Tagged_union).
+
+An example sum type definition in Haskell
+
+```haskell
+
+data Either a b = Left a | Right b
+```
+### Record types
+
+A record type is essentially a product type where each field is accompanied by a
+field name (https://en.wikipedia.org/wiki/Product_type)
+
+### Product types
+
+A product type is a tuple of types.
+
+### Recursive types
+
+Recursive types are types that are defined in terms of themselves.
+
+```haskell
+
+data List a = Nil | Cons a (List a)
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+```
+
 ## References 
 
 - https://json-schema.org/implementations.html

docs/compiler.md

@@ -1,4 +1,4 @@
-# LambdaBuffers _Compiler_ Spec & Design
+# LambdaBuffers Compiler
 
 The _Compiler_ component sits between the _Frontend_ component and the code
 generation component named _Codegen_. The purpose of the _Compiler_ is to
@@ -12,7 +12,7 @@ The end goal of the _Compiler_ is to ensure that the _Codegen_ component is
 capable of processing the _Compiler Output_ by providing correct and complete
 information.
 
-## _Compiler_ interface
+## Compiler Interface
 
 The _Compiler_ operates on the _Compiler Input_ message specified in the
 [compiler.proto](../lambda-buffers-proto/compiler.proto) [Google Protocol
@@ -28,7 +28,7 @@ communicating via [Google Protocol Buffers](https://protobuf.dev/).
 Refer to the [Compiler Proto
 documentation](../lambda-buffers-proto/compiler-proto.md) for more information.
 
-## Checking type definitions (kind checking)
+## Checking Type Definitions
 
 The first step the Compiler performs is _kind checking and inference_ on [type
 definitions](../lambda-buffers-proto/compiler-proto.md#lambdabuffers-compiler-TyDef)
@@ -40,9 +40,9 @@ term](../lambda-buffers-proto/compiler-proto.md#lambdabuffers-compiler-Ty) with
 [kind](../lambda-buffers-proto/compiler-proto.md#lambdabuffers-compiler-Kind)
 information.
 
-In standard _type checking_ terminology LambdaBuffers terms are [abstract data
+In standard _type checking_ terminology LambdaBuffers 'terms' are [abstract data
 type](https://en.wikipedia.org/wiki/Abstract_data_type) declarations and their
-types are kinds.
+'types' are _kinds_.
 
 Currently, the _Compiler_ accepts:
 
@@ -64,7 +64,54 @@ 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`.
 
-## Checking type cardinality
+### Kind Checker
+
+The kind checker is designed around a simply typed lambda calculus type system
+with inference via unification (_John Alan Robinson's_ unification algorithm is
+being currently used). We've also introduced a `let` binding rule that allows
+later additions to the typing context. The typing rules are the following:
+
+```text
+ x : σ ∈ Γ
+----------- [Variable]
+ Γ ⊢ x : σ
+
+
+      Γ,x:σ ⊢ e:τ
+------------------------ [Abstraction]
+ Γ ⊢ (λ x:σ. e):(σ → τ)
+
+
+Γ ⊢ x:(σ → τ)    Γ ⊢ y:σ
+------------------------- [Application]
+       Γ ⊢ x y : τ
+
+
+Γ ⊢ e₁:σ    Γ, e₁ : σ ⊢ e₂:τ
+----------------------------- [Let]
+   Γ ⊢ let x = e₁ in e₂ : τ
+```
+
+The type checking strategy is as follows:
+
+1. A context is built from the type definitions. Type variables which are not
+   annotated with any further kind information are defaulted to be of kind
+   `Type`.
+
+2. The RHS of the type terms are converted into their _Sums of Products_
+   canonical representation. The variables from the left hand side of the term
+   are introduced to the right hand side as abstractions.
+
+3. The derivation for each term is built.
+
+4. Then the unification tries to find a solution.
+
+Terms for which unification cannot find a consistent derivation are deemed
+incorrect and a kind checking error is thrown. Note that currently all of the
+inferred kinds have a restriction to be monomorphic - therefore no free or
+universally quantified variables can appear in the final kind signature.
+
+## Checking Type Cardinality
 
 In addition to _kind checking_, the Compiler could perform a special check for
 types to determine their cardinality. This is especially useful to catch and
@@ -78,7 +125,7 @@ ill-defined.
 This problem is equivalent to a problem of [calculating graph
 components](https://en.wikipedia.org/wiki/Component_(graph_theory)).
 
-## Normalizing type definitions
+## Normalizing Type Definitions
 
 Finally, the compiler should be able to _normalize_ expressions. For example, it
 may be possible to define a data type in the schema language in a form similar
@@ -87,7 +134,7 @@ the order of application within the term. The example term would normalize to
 `data G a = G (Either (Maybe a) Int)` - resulting in a cleaner (and more
 performant) code generation.
 
-## Checking typeclass definitions and instance clauses
+## Checking Typeclass Definitions and Instance Clauses
 
 The _Compiler_ should, if possible, ensure that all instance declarations for
 schemata are derivable using hard-coded derivation axioms.
@@ -132,56 +179,4 @@ sufficiently rich to express typeclass relations, we will generate instances
 using idiomatic language features. (The details will depend on the particular
 language.)
 
-## Kind Checker
-
-The kind checker is designed around a simply typed lambda calculus type system
-with inference via unification (_John Alan Robinson's_ unification algorithm is
-being currently used). We've also introduced a `let` binding rule that allows
-later additions to the typing context. The typing rules are the following:
-
-```text
- x : σ ∈ Γ
------------ [Variable]
- Γ ⊢ x : σ
-
-
-      Γ,x:σ ⊢ e:τ
------------------------- [Abstraction]
- Γ ⊢ (λ x:σ. e):(σ → τ)
-
-
-Γ ⊢ x:(σ → τ)    Γ ⊢ y:σ
-------------------------- [Application]
-       Γ ⊢ x y : τ
-
-
-Γ ⊢ e₁:σ    Γ, e₁ : σ ⊢ e₂:τ
------------------------------ [Let]
-   Γ ⊢ let x = e₁ in e₂ : τ
-```
-
-The type checking strategy is as follows:
-
-1. A context is built from the type definitions. Type variables which are not
-   annotated with any further kind information are defaulted to be of kind
-   `Type`.
-
-2. The RHS of the type terms are converted into their _Sums of Products_
-   canonical representation. The variables from the left hand side of the term
-   are introduced to the right hand side as abstractions.
-
-3. The derivation for each term is built.
-
-4. Then the unification tries to find a solution.
-
-Terms for which unification cannot find a consistent derivation are deemed
-incorrect and a kind checking error is thrown. Note that currently all of the
-inferred kinds have a restriction to be monomorphic - therefore no free or
-universally quantified variables can appear in the final kind signature.
-
-## Unsolved Problems
-
-- [ ] How would cardinality checking be integrated within our current checking
-      strategy?
-
 ## Missing link

docs/design.md

@@ -1,10 +1,10 @@
-# LambdaBuffers design
+# LambdaBuffers Design
 
 The goal of the LambdaBuffers project is to enable software developers to
 specify their application types in a common format that can be conveniently
 shared and their values effectively communicated across language barriers.
 
-## Problem statement
+## Problem Statement
 
 Software projects that span multiple language environments often interact in a
 sub-optimal manner. Significant effort is spent in making application messages
@@ -27,7 +27,7 @@ costs to the business and unsustainable technical debt.
 5. Universally consistent semantics,
 6. Modular API architecture.
 
-### Expressive types
+### Expressive Types
 
 Application types that users can define should be expressive enough to
 facilitate type driven domain modeling and to express application
@@ -43,7 +43,7 @@ parameterized, effectively enabling generic types. LambdaBuffers also supports
 recursive type definitions, which allow users to succinctly define elegant and
 expressive data structures.
 
-### Expressive semantics annotation
+### Expressive Semantics Annotation
 
 Enabling users to manage the *semantics* associated with their types is
 essential for adapting LambdaBuffers to a variety of different domains and use
@@ -82,7 +82,7 @@ document for a given type class.
 For each new type class declared, code generation tooling must be updated to
 handle the new type class.
 
-### Extensible to new types
+### Extensible to New Types
 
 Enabling users to introduce new *built-in* types allows LambdaBuffers to be
 adapted in many different domains and use cases.
@@ -105,7 +105,7 @@ equipped with rich libraries that work with them. Redefining them *ab ovo* would
 be counterproductive as users would have to re-implement and reinvent the rich
 support for such types.
 
-### Extensible to new semantics
+### Extensible to New Semantics
 
 Enabling users to introduce new *type semantics* facilitates LambdaBuffers to be
 adapted in many different domains and use cases.
@@ -134,7 +134,7 @@ provide code generation modules for a set of officially supported language
 environments. However, modular design will hopefully facilitate community
 contributions in a sustainable fashion.
 
-### Universally consistent semantics
+### Universally Consistent Semantics
 
 The types specified by users must be handled in a compatible manner across
 language environments. This is a critical requirement that underpins this
@@ -150,7 +150,7 @@ LambdaBuffers does not provide a way to formally verify consistency across langu
 however, a comprehensive test suite will be developed to ensure that new code
 generation modules are indeed implemented correctly.
 
-### Modular API architecture
+### Modular API Architecture
 
 LambdaBuffers establishes three separate components of the architecture, namely
 *Frontend*, *Compiler* and *Codegen**.

docs/feedback/interview-notes.md

@@ -14,7 +14,7 @@
 1. Introduction - what is Lambda Buffers and what is Lambda Buffers' aim.
 2. Interviews
 
-## Meeting minutes
+## Meeting Minutes
 
 1. Drazen introduces what Lambda Buffers is, and how it relates to the target languages. Points touched on:
     1. Tooling