syntaxAlchemist/lib-laddertypes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

README: minor improvements

Browse source
This commit is contained in:
Michael Sippel 2023-10-03 04:34:47 +02:00
parent f45593cfd5
commit aacafb318a
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 14 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
README.md
View file

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