From 6079d2ece166b3c50de23564614fa5c9c2ca14db Mon Sep 17 00:00:00 2001 From: Alexander Nutz Date: Mon, 15 Sep 2025 12:19:40 +0200 Subject: [PATCH] wip --- spec.md | 253 ++++++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 229 insertions(+), 24 deletions(-) diff --git a/spec.md b/spec.md index cdf6d78..fd6175e 100644 --- a/spec.md +++ b/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 -# result: 5.8 +type Illegal1 = &a a + +type Illegal2 = &a {x: a, y: Int8} ``` -## Few types to learn -Most important ones: -- `Num`: big-decimal -- `List[T]`: (linked-) list of `T` -- `Char`: unicode codepoint -- `Unit`: nothing -- `i -> o`: function -- `template a, b: t` +The definition of "infinite size" is: +- for records: if _any_ of the field types has "infinite size" +- for unions: if _all_ of the cases has "infinite size" +- for functions: never +- for recursive types: + - if the type was already visited: yes + - otherwise: if the inner type has "infinite size" -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 + +
+Example + +Compilation unit 1: ``` -# the type of msg is: List[Char] -> List[Char] -def msg(username: List[Char]) -> List[Char] { - "Hello, " ++ username ++ "!" # last expr is returned -} +type ?Uint8 = {field:type} +type Uint8 = {...?Uint8} -# the type of main is: Unit -> IO[Unit] -def main() -> IO[Unit] { - print("hi") -} +# this compilation does not have the limitations of partial types, because the definition for `?Uint8` is available ``` +Compilation unit 2: +``` +type Uint8 = {...?Uint8} +``` + +
+ + +## Syntax +TODO ebnf + + +## Compatible-with +TODO + + +## Phi unification +TODO + + + +# "Platform library" +Depends on on the [core library](#core-library). + +Platform / language implementation / target depedent. + +
+Signature + +``` +############ 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} +``` + +
+ + +# "Core library" +Depend on the [platform library](#platform-library). + +Completely platform, language implementation, and target independent. + +
+Signature + +``` +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 +``` + +
+ +
+Reference Implementation + +TODO + +
+ + + +# "Standard library" +Depend on the [platform library](#platform-library) and [core library](#core-library). + +Responsible for IO + +
+Signature + +``` +############ 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 +``` + +
+ +
+Implementation snippets + +TODO: example definition of IO + +
+ + +# (top-level) declarations +TODO + +TODO: add either attribute system, or comptime exec + + +# Expressions +TODO + + + + + + + +# OLD SPECIFICATION STARTING HERE + + ## Anonymus functions ``` The type of List.map is List[t] -> (t -> t) -> List[t]