From 74075b4612ce31191ca951549808f09d54392680 Mon Sep 17 00:00:00 2001 From: Alexander Nutz Date: Mon, 15 Sep 2025 16:15:23 +0200 Subject: [PATCH] new spec done soon --- spec.md | 255 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 128 insertions(+), 127 deletions(-) diff --git a/spec.md b/spec.md index fd6175e..a09a699 100644 --- a/spec.md +++ b/spec.md @@ -73,12 +73,44 @@ TODO ebnf ## Compatible-with -TODO +Check if type is compatible-with / assignable-to type requirements. + +- a type is compatible with itself ofcourse +- a tagged union is compatible with anothr, + if the other one contains at least all cases from this union, + and those cases are compatible +- a non-nominal record is compatbile with anohter, + if the other one contains a _subset_ of the fields of this one, + and the field types are comptible. +- a type is compatible with a partial type `?Ty`, + if the definition of the partial type is in the current scope, + and the type is compatible with the type inside the definition +- partial records and unions are similar to the above. + +TODO: need more details? ## Phi unification -TODO +This process is performed on the resulting types of two merging branches +Tries, in order: +- if one of the types is a tagged union, + which contains only one case with an identical type, + and the other is not a tagged union, + it will "attach" that case onto the other type, like this: + `'N Num | 'I Int` and `Num` -> `'N Num | 'I Int` +- if one of the types is a tagged union with exactly one case, + and the other one is not an union, + it will put that tag onto it, and phi-merge the inner types. + example: `'N Num` and `Num` -> `'N Num` +- if both types are tagged unions, + the result is an tagged union contain the csaes of both tagged unions. + union cases that are in both branches, will have their types phi-unified too. + example: `'Ok ('N Num | 'I Int) | 'SomeErr` and `'Ok Num | 'AnotherErr` -> `'Ok ('N Num) | 'SomeErr | 'AnotherErr` +- if both types are non-nominal records, + the result will contain only fields that are present in both types. + The types of the fields will get phi-unified too + example: `{a:Num,b:Num,c:Num}` and `{a:Num,c:Num,e:Num}` -> `{a:Num, e:Num}` # "Platform library" @@ -96,7 +128,6 @@ 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} ``` @@ -137,6 +168,36 @@ def Bool.xor : Bool -> Bool -> Bool ## arbitrary-precision signed decimal number type Num +def Num.toStr : Num -> Char List + +# consider using locale aware, and space ignoring parsing instead +# parses of format 123 / -123 / 123.456 +def Num.parseLit : Char List -> Num Option + +def Num.zero : Num +def Num.one : Num + +def `a+b` : Num -> Num -> Num +def `a-b` : Num -> Num -> Num +def `a*b` : Num -> Num -> Num +def `a/b` : Num -> Num -> Num + +def Num.neg : Num -> Num + + +############ Char ############ +# one unicode codepoint +type Char +def Char.toAscii : Char -> Uint8 Option +def Char.fromAscii : Uint8 -> Char Option +def Char.encodeUtf8 : Char -> Uint8 List +def Char.decodeUtf8 : Uint8 List -> 'Cons {v: Char, next: Uint8 List} + + +############ String ############ +def String.encodeUtf8 : Char List -> Utf8 List +def String.decodeUtf8 : Uint8 List -> 'Ok Char List | 'Err {at: Num} + ############ t List ############ ## A generic linked-list type @@ -224,140 +285,80 @@ TODO TODO: add either attribute system, or comptime exec +# Mostly forward type inference +Exception 1: +``` +def List.map : t List -> (t -> r) -> r List + +# doesn't require specifying types in lambda: simple one-step backwards type inference +List.map([1,2,3], x -> x * 2) +``` + +Exception 2: +``` +def add : Num -> Num -> Num = + a -> b -> a + b +# ^^^^^^ +# does not require specification of those types, because already specified in function signature + +# this also applies to: + +def add : Num -> Num -> Num +def add = a -> b -> a + b +``` + + # Expressions +- `expr:field` access field from non-nominal record +- `let varName = value exprUsingTheVar` +- `'a'` unicode codepoint literal, aka "char" literal. returns a `Char` +- `[1,2,3]` list literal: creates a `t List`, where `t` is equal to the type of all the wrapped expressions +- `"Hello\\nworld"` string literal with escape characters. same behaviour as list literal of the chars +- `12.345`, or `12`, or `-12`: same behaviour as `Num.parseLit` on the value (as string) +- `arg -> value`: one-step backwards inferrable lambda +- `arg: Type -> value` +- `func(arg1, arg2)`: function application. requires at least one argument. partial function applications are allowed too +- `expr :: type`: down-cast type +- `recExpr with fieldname: newFieldValue`: overwrites or adds a field to a record type. + type checking: identical to `recExpr and {fieldname: newFieldValue}` +- `recExpr and otherRecExpr`: "sum" fields together of both record expressions. + type checking: phi-unify `recExpr` with `otherRecExpr`, and require that both are non-nominal record types +- `if cond then a else b` +- `{field1: val1, field2: val2}` field construction +- `match expr with `: [pattern matching](##pattern-matching) +- `a = b` the [equality operator](##equality-operator) +- `a + b`: identical to `\`a+b\`(a, b)` name: "sum" +- `a - b`: identical to `\`a-b\`(a, b)` name: "difference" +- `a * b`: identical to `\`a*b\`(a, b)` name: "times" +- `a / b`: identical to `\`a/b\`(a, b)` name: "over" +- `a ++ b`: identical to `\`a++b\`(a,b)` name: "list concatenate" +- `a => b`: identical to `\`a=>b\`(a,b)` name: "lens compose" + + +## pattern matching TODO +## equality operator +The only operator with type overloading + +TODO +# coding patterns (for users only) +## labelled arguments +``` +def List.remove_prefix(prefix: t List, list: 'from t List) + +List.remove_prefix([1,2], 'from [1,2,3,4]) + +# but this also works most of the times: +List.remove_prefix([1,2], [1,2,3,4]) +``` # OLD SPECIFICATION STARTING HERE - - -## Anonymus functions -``` -The type of List.map is List[t] -> (t -> t) -> List[t] -List.map(li, x:Num -> x * 2) -``` - -## Simple, forward type-inference -``` -def zero () -> Flt32 { - 3.1 # error: got Num, but expected Flt32 -} -``` - -## Partial function applications -``` -# type of add is Num -> Num -> Num -def add(a: Num, b: Num) -> Num { - a + b -} - -let a = add(1) # type of a is Num -> Num -let b = a(2) # type of b is Num -# b is 3 -``` - -## Bindings -``` -let name = "Max" -let passw = "1234" -``` - -## no confusing function or operator overloading -all operators: -- `Num + Num` (has overloads for fixed width number types) -- `Num - Num` (has overloads for fixed width number types) -- `Num * Num` (has overloads for fixed width number types) -- `Num / Num` (has overloads for fixed width number types) -- `Num ^ Num`: raise to the power (has overloads for fixed width number types) -- `List[t] ++ List[t]`: list concatenation -- `value :: t` (explicitly specify type of value, useful for down-casting structs, or just code readability; does not perform casting) -- `list[index]` -- `a => b`: lens compose - -## non-nominal struct types -``` -# `type` creates a non-distinct type alias -type User = { name: List[Char] } -type DbUser = { name: List[Char], pass: List[Char] } - -def example4(u: User) -> List[Char] { - u:name # colon is used to access fields -} - -def example(u: User) -> DbUser { - u with pass: "1234" - # has type { name: List[Char], pass: List[Char] } -} - -def example2() -> {name: List[Char], pass: List[Char]} { - {name:"abc", pass:"123"} -} - -def example3() -> User { - example2() # {name:.., pass:...} can automatically decay to {name:...} -} -``` - -## (tagged) union types -``` -type Option[t] = - 'Err # If no type specified after tag, defaults to Unit -| 'Some t - -# the tags of unions are weakly attached to the types, but won't decay unless they have to -def example(n: Num) -> Num { - let x = 'MyTag n # type of x is 'MyTag Num - x # tag gets removed because target type is Num -} - -def example2(n: Num) -> Option[Num] { - 'Some n -} - -def example3-invalid() -> Option[Num] { - Unit # error: can't convert type `Unit` into type `'Err Unit | 'Some Num` - # Either label the expression with 'Err, - # or change the return type to Option[Unit], and label the expression with 'Some -} - -def exampe4() -> Option[Num] { - 'Err Unit - # type of this expression is: `'Err Unit` - # enums can automatically cast, if all the cases from the source enum also exists in the target enum, - # which they do here: `'Err Unit` is a case in `'Err Unit | Num` -} - -def example5-error() -> Option[Num] { - let x = ( 'Err Unit ) :: Option[Unit] - x - # error: can't convert type `'Err Unit | 'Some Unit` into type `'Err Unit | 'Some Num` - # The case `'Some Unit` does not exist in the target `'Err Unit | 'Some Num` -} - -def example6-error() -> Option[Unit] { - let x = 'Error Unit - x - # in this case, the enum tag does not decay, like in `example`, - # because we are casting to an enum - - # error: can't convert type `'Error Unit` into type `'Err Unit | 'Some Num`` - # 1st possible solution: manually cast to just `Unit` (via `expr :: Unit`), so that it can convert to the second case of the target - # 2nd possible solution: pattern match against the enum, to rename the tag from 'Error to 'Err -} -``` - -### pattern 1: labelled arguments -``` -def [t] List.remove_prefix(prefix: List[t], list: 'from List[t]) - -List.remove_prefix([1,2], 'from [1,2,3,4]) -``` - ## automatic return types ``` def add(a: Num, b: Num) -> _ {