Open HoshinoTented opened 2 years ago
if our lambda syntax is:
box lambda <- { a; b; c ->
** do something
}.
then I am happy to use this syntax as generics syntax:
box { t; s; r ->
field_t: t,
field_s: s,
field_r: r,
}: some_type.
However, Kotlin's lambda syntax is pretty, but I want to differ from it.
why not:
box [a; b; c] {
** ...
}: some_type.
idea from coq: if the compiler is unable to infer a type for some type parameter, developers can just specify a type for that type parameter (but not all), like:
** foo: [a; b; c; d][a; b; c] -> d
** foo[1; 2; 3]. the compiler can not choose a type for the type parameter 'd'
foo[d <- i32][1; 2; 3].
** or
foo[_; _; _; i32][1; 2; 3].
the arguments for one magic have two parts: type parameter and normal parameter. for example:
magic foo[i: i32] {
i
}: i32.
** foo has a singature: [i32] -> i32
** it is equivalent to [][i32] -> i32, the type parameter list is empty
magic bar[a][i: a] {
i
}: a.
** bar has a signature: [a][a] -> a.
** first 'a' is the name of the type parameter, the second one is the type of parameter.
idea from coq: if the compiler ...
for the sake of simplicity, we can only support the second one.
why not:
box [a; b; c] { ** ... }: some_type.
I prefer this version, box [a; b; c] {}: some_type.
is similar to the magic declaration, and type declaration is a magic on type:
accepts type as its parameter and returns a type!
But the empty space between the box
keyword and the Type Parameter list is weird.
I forgot...
Use this instead.
box some_type [a; b; c] {
** ...
}.
If : some_type
is the return type then it should be a type of type.
What is the syntax of member magic
?
What is the syntax of
member magic
?
I think I will use a rust-like way...
Enumerate Structure:
box option [a]
| some { value : a }
| none
In fact, I want to make this OCaml-like syntax more HNM-like:
box option [a] {
| some { value : a }
| none
** or (the beginning "|" is optional)
some { value : a } | none
}.
or
box option [a] <- some { value : a } | none. ** This looks like a variable declaration, which is ambiguous.
** Again, the beginning "|" is optional.
Pattern Matching would like:
match (some_option) {
** Optional beginning "|"
| some { value } => ...
| none => ...
}
** or
match (some_option) {
| some { value: v } => ...
| none => ...
}
Non-exhaustive matching is now allowed.
Concept (aka Trait):
concept concept_name [ type_parameters ] {
** `concept` keyword can be simplified to `con`
magic magic_in_concept [ ... ] [ ... ] -> ...
magic magic_with_default_impl [ ... ] [ ... ] { ... }: ...
** a magic with self is similar to the Rust one, however, there is no ownership in HNM, so `self` impleis copy, `~self` implies referencing
magic magic_with_self [ ... ] [ self ; ... ] -> ...
}.
Impl Concept:
** use `Concat` keyword
concat concat_name [ type_parameters ] {
** `concat` keyword can be simplified to `nya`
** concat_name can be omitted
** implementations...
magic magic_in_concept [ ... ] [ ... ] { ... }: ...
** no need to impl a magic that has a default implementation
magic magic_with_self [ ... ] [ self ; ... ] {
** self has type: type_name [ ... ]
}: ...
}: type_name [ ... ] -> concept_name [ ... ].
Concat is a connection between types and concepts, this syntax provided the possibility of multi-implementation between the same type and the same concept.
If the compiler found only one Concat or the concat name was omitted, that Concat was used. If there is an unnamed Concat, then Multiple Concat is disallowed.
Multi-Impl
area natural.
con say_hello {
magic hello [ self ] -> unit.
}.
nya concat1 {
magic hello [ self ] {
natural->emit["Hello: " + self->to_string[]].
}.
}: i32 -> say_hello.
nya concat2 {
magic hello [ self ] {
natural->emit["Hi: " + self->to_string[]].
}.
}: i32 -> say_hello.
magic center [] {
box i <- 1.
** i->hello[]. ** Compile error. There are multiple concats of i32.
concat1[i]->hello[]. ** print "Hello: 1"
concat2[i]->hello[]. ** print "Hi: 1"
}
con
sounds like a Kitsune and nya
sounds like a Neko.
The Concat
Syntax is not friendly to IDE, we have to write the "return type" first for the ide prompt
box type_name [ type_parameter_scope ] {
** type scope
constructor0 {
** constructor scope
}
}
constructor_name { ... }
: Declaring a constructor|
: Another constructorfield : type
: Declaring a fieldsuper :< type
: Declaring a supertypeThe syntax like xxx {}: ttt.
limits coding habits, it encourages people writing it in (the underline is the focus):
xxx {}: ttt_
then (moving focus):
xxx {_}: ttt
finally (inserting a new line):
xxx {
_}: ttt
This is interesting, I didn't think about these anytime. However, I think this is good.
Built-in Types
Type Declaration
Usage
Generics Type Declaration
Usage