wip
This commit is contained in:
253
spec.md
253
spec.md
@@ -1,36 +1,241 @@
|
|||||||
## Arithmetic
|
# Contribution Guidelines
|
||||||
|
- explain why design decisions are taken
|
||||||
|
- put in `TODO`s into the specification for things that should be re-visited in the future
|
||||||
|
|
||||||
|
|
||||||
|
# Goals
|
||||||
|
- functional programming: everything is pure, and only a function
|
||||||
|
- easy to learn, even as first programming language
|
||||||
|
- only one way of doing things. not 20. Eg: onle list type, instead of 20
|
||||||
|
- pretty easy to implement
|
||||||
|
|
||||||
|
|
||||||
|
# Data types
|
||||||
|
One of:
|
||||||
|
- `t -> t`: pure function taking `t` as argument, and returning `t`
|
||||||
|
- `{ field1: xt, field2: yt }`: non-nominal records
|
||||||
|
- `'Case1 t | 'Case2 t2 | 'Case3 t3`: tagged unions
|
||||||
|
- `with myGenericName: x`: introduce "generic" type `myGenericName`, which can be used in type `x`
|
||||||
|
- `&a 'EOL | 'Cons {v: t, next: a}`: [recursive type](##recursive-types)
|
||||||
|
- `?Identifier`: the partial type `Identifier`
|
||||||
|
- `'Case1 t1 | 'Case2 t2 | ...?Identifier`: partial tagged union type, `Identifier`
|
||||||
|
- `{field1: xt, field2: yt, ...?Identifier}`: partial non-nominal record type, `Identifier`
|
||||||
|
|
||||||
|
## Recursive types
|
||||||
|
Recursive / self-referential types
|
||||||
|
|
||||||
|
These are not allowed to have an infinite size, for example these are illegal:
|
||||||
```
|
```
|
||||||
1.2 * 4 + 1
|
type Illegal1 = &a a
|
||||||
# result: 5.8
|
|
||||||
|
type Illegal2 = &a {x: a, y: Int8}
|
||||||
```
|
```
|
||||||
|
|
||||||
## Few types to learn
|
The definition of "infinite size" is:
|
||||||
Most important ones:
|
- for records: if _any_ of the field types has "infinite size"
|
||||||
- `Num`: big-decimal
|
- for unions: if _all_ of the cases has "infinite size"
|
||||||
- `List[T]`: (linked-) list of `T`
|
- for functions: never
|
||||||
- `Char`: unicode codepoint
|
- for recursive types:
|
||||||
- `Unit`: nothing
|
- if the type was already visited: yes
|
||||||
- `i -> o`: function
|
- otherwise: if the inner type has "infinite size"
|
||||||
- `template a, b: t`
|
|
||||||
|
|
||||||
Advanced (uncommon) types:
|
|
||||||
- `Int8`, `Int16`, ...
|
|
||||||
- `Uint8`, ...
|
|
||||||
- `Flt32`, `Flt64`
|
|
||||||
|
|
||||||
## Functions
|
## Partial types
|
||||||
|
These are types where the full definition is somewhere else (eg another compilation unit)
|
||||||
|
|
||||||
|
This type naturally adds limitations:
|
||||||
|
- for partial non-nominal records: these can not be constructed with the record construct expression
|
||||||
|
- for partial unions: they can not be pattern matched exhaustively
|
||||||
|
|
||||||
|
these limitations are removed, if the full definition is in the current scope
|
||||||
|
|
||||||
|
<details>
|
||||||
|
<summary>Example</summary>
|
||||||
|
|
||||||
|
Compilation unit 1:
|
||||||
```
|
```
|
||||||
# the type of msg is: List[Char] -> List[Char]
|
type ?Uint8 = {field:type}
|
||||||
def msg(username: List[Char]) -> List[Char] {
|
type Uint8 = {...?Uint8}
|
||||||
"Hello, " ++ username ++ "!" # last expr is returned
|
|
||||||
}
|
|
||||||
|
|
||||||
# the type of main is: Unit -> IO[Unit]
|
# this compilation does not have the limitations of partial types, because the definition for `?Uint8` is available
|
||||||
def main() -> IO[Unit] {
|
|
||||||
print("hi")
|
|
||||||
}
|
|
||||||
```
|
```
|
||||||
|
|
||||||
|
Compilation unit 2:
|
||||||
|
```
|
||||||
|
type Uint8 = {...?Uint8}
|
||||||
|
```
|
||||||
|
|
||||||
|
</details>
|
||||||
|
|
||||||
|
|
||||||
|
## Syntax
|
||||||
|
TODO ebnf
|
||||||
|
|
||||||
|
|
||||||
|
## Compatible-with
|
||||||
|
TODO
|
||||||
|
|
||||||
|
|
||||||
|
## Phi unification
|
||||||
|
TODO
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
# "Platform library"
|
||||||
|
Depends on on the [core library](#core-library).
|
||||||
|
|
||||||
|
Platform / language implementation / target depedent.
|
||||||
|
|
||||||
|
<details>
|
||||||
|
<summary>Signature</summary>
|
||||||
|
|
||||||
|
```
|
||||||
|
############ Primitive Data types ############
|
||||||
|
type Uint8
|
||||||
|
|
||||||
|
def Uint8.wrapping_add : Uint8 -> Uint8 -> Uint8
|
||||||
|
def Uint8.bitwise_not : Uint8 -> Uint8
|
||||||
|
def Uint8.less_than : Uint8 -> Uint8 -> Bool
|
||||||
|
def Uint8.equal : Uint8 -> Uint8 -> Bool
|
||||||
|
def Uint8.bits : Uint8 -> {7:Bool,6:Bool,5:Bool,4:Bool,3:Bool,2:Bool,1:Bool,0:Bool}
|
||||||
|
```
|
||||||
|
|
||||||
|
</details>
|
||||||
|
|
||||||
|
|
||||||
|
# "Core library"
|
||||||
|
Depend on the [platform library](#platform-library).
|
||||||
|
|
||||||
|
Completely platform, language implementation, and target independent.
|
||||||
|
|
||||||
|
<details>
|
||||||
|
<summary>Signature</summary>
|
||||||
|
|
||||||
|
```
|
||||||
|
type Unit = {}
|
||||||
|
|
||||||
|
|
||||||
|
######### Primitive storage-only types ##########
|
||||||
|
type Int8 = Uint8
|
||||||
|
type Int16 = {hi:Int8, lo:Int8}
|
||||||
|
type Int32 = {hi:Int16, lo:Int16}
|
||||||
|
type Int64 = {hi:Int32, lo:Int32}
|
||||||
|
type Int128 = {hi:Int64, lo:Int64}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
############ Bool ############
|
||||||
|
type Bool = 'True | 'False
|
||||||
|
def Bool.not : Bool -> Bool
|
||||||
|
def Bool.and : Bool -> Bool -> Bool
|
||||||
|
def Bool.or : Bool -> Bool -> Bool
|
||||||
|
def Bool.nor : Bool -> Bool -> Bool
|
||||||
|
def Bool.xor : Bool -> Bool -> Bool
|
||||||
|
|
||||||
|
|
||||||
|
############ Num ############
|
||||||
|
## arbitrary-precision signed decimal number
|
||||||
|
type Num
|
||||||
|
|
||||||
|
|
||||||
|
############ t List ############
|
||||||
|
## A generic linked-list type
|
||||||
|
type t List = 'EOL | 'Cons {v: t, next: t List}
|
||||||
|
|
||||||
|
## List concatenate
|
||||||
|
def `a++b` : t List -> t List -> t List
|
||||||
|
|
||||||
|
## Get nth element
|
||||||
|
def List.nth : t List -> Num -> t Option
|
||||||
|
|
||||||
|
|
||||||
|
############ t Option ############
|
||||||
|
type t Option = 'None | 'Some t
|
||||||
|
```
|
||||||
|
|
||||||
|
</details>
|
||||||
|
|
||||||
|
<details>
|
||||||
|
<summary>Reference Implementation</summary>
|
||||||
|
|
||||||
|
TODO
|
||||||
|
|
||||||
|
</details>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
# "Standard library"
|
||||||
|
Depend on the [platform library](#platform-library) and [core library](#core-library).
|
||||||
|
|
||||||
|
Responsible for IO
|
||||||
|
|
||||||
|
<details>
|
||||||
|
<summary>Signature</summary>
|
||||||
|
|
||||||
|
```
|
||||||
|
############ IO ############
|
||||||
|
type t IO
|
||||||
|
def IO.just : t -> t IO
|
||||||
|
def IO.chain : t IO -> (t -> r IO) -> r IO
|
||||||
|
|
||||||
|
|
||||||
|
############ Stream ############
|
||||||
|
# represents a non-seekable t-stream, for example a tcp stream
|
||||||
|
type t io.Stream
|
||||||
|
|
||||||
|
TODO: networking api: stream and datagram protocols
|
||||||
|
|
||||||
|
|
||||||
|
############ Path ############
|
||||||
|
# paths are not absolute, but rather relative to any reference point
|
||||||
|
type io.Path = {parent: io.Path Option, ...?io.Path}
|
||||||
|
def io.Path.eq : io.Path -> io.Path -> Bool
|
||||||
|
def io.Path.root : io.Path -> io.Path
|
||||||
|
def io.Path.child : io.Path -> Char List -> io.Path Option
|
||||||
|
|
||||||
|
TODO: links, permissions, ... etc
|
||||||
|
|
||||||
|
|
||||||
|
############ File ############
|
||||||
|
type io.ReadFile
|
||||||
|
type io.WriteFile
|
||||||
|
|
||||||
|
type t io.FileOpenResult = 'Ok t | 'CantReopenThis | 'FileNotFound | 'PermissionError | 'OtherErr
|
||||||
|
def io.file.open.r : io.Path -> io.ReadFile io.FileOpenResult
|
||||||
|
def io.file.open.w : io.Path -> io.WriteFile io.FileOpenResult
|
||||||
|
def io.file.open.rw : io.Path -> {r: io.ReadFile, w: io.WriteFile} io.FileOpenResult
|
||||||
|
|
||||||
|
TODO: read, write, extend, truncate
|
||||||
|
```
|
||||||
|
|
||||||
|
</details>
|
||||||
|
|
||||||
|
<details>
|
||||||
|
<summary>Implementation snippets</summary>
|
||||||
|
|
||||||
|
TODO: example definition of IO
|
||||||
|
|
||||||
|
</details>
|
||||||
|
|
||||||
|
|
||||||
|
# (top-level) declarations
|
||||||
|
TODO
|
||||||
|
|
||||||
|
TODO: add either attribute system, or comptime exec
|
||||||
|
|
||||||
|
|
||||||
|
# Expressions
|
||||||
|
TODO
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
# OLD SPECIFICATION STARTING HERE
|
||||||
|
|
||||||
|
|
||||||
## Anonymus functions
|
## Anonymus functions
|
||||||
```
|
```
|
||||||
The type of List.map is List[t] -> (t -> t) -> List[t]
|
The type of List.map is List[t] -> (t -> t) -> List[t]
|
||||||
|
Reference in New Issue
Block a user