diff --git a/README.md b/README.md index 46fd427..d4dc395 100644 --- a/README.md +++ b/README.md @@ -6,20 +6,21 @@ Rust Implementation of Ladder-Types (parsing, unification, rewriting, etc) ## Ladder Types In order to implement complex datastructures and algorithms, usually -many layers of abstraction are built ontop of each other, and -consequently higher-level data types are encoded into lower-level data +many layers of abstraction are built ontop of each other. +Consequently higher-level data types are encoded into lower-level data types, forming a chain of embeddings from concept to `rock bottom' of -byte streams. While a high-level type makes claims about an objects -semantics, it is ambiguous in regard to its concrete syntactical -representation or memory layout. However these concrete -representational forms must be compatible for type-safe compositions. +byte streams. While a high-level type makes claims about the +semantics of objects of that type, high-level types are ambiguous in +regard to their concrete syntactical representation or memory +layout. However for compositions to be type-safe, compatibility of +concrete represenations must be ensured. -For example in the unix shell, many different tools & utilities exist -concurrently and depending on the application domain, each will -potentially make use of different representational forms. Abstract -concepts like 'natural number' could exist in many representational -forms, e.g. with variation over radices, endianness, digit encoding -etc. +For example in the unix shell, many different tools & utilities +coexist. Depending on the application domain, each of them will +potentially make use of different representational forms for the same +abstract concepts. E.g. for the concept 'natural number', many +representations do exist, e.g. with variation over radices, +endianness, digit encoding etc. Intuitively, *ladder types* provide a way to distinguish between multiple *concrete representations* of the same *abstract / conceptual @@ -37,7 +38,7 @@ each represented as unix-timestamp written as decimal number in big-endian, encoded as UTF-8 string. ``` - ~ ~ℕ