dannypsnl / eikyo

polymorphsim language with mark system

(information
  #:name (cond [(know-taiwanese? you) "Lîm Tsú-thuàn"]
               [(know-chinese? you) "林子篆"]
               [else "Danny"])
  #:focus-on '(PLT Networking OS)
  #:language '(ocaml elixir haskell racket)
  #:prover '(lean agda)
  #:learning '(inductive families
               natural model
               modules, dependencies, and cache format
               terimation property: sized/glued dependent type
               modal logic & its properties)
  #:mail "[email protected]"
  #:pronouns: '(He Him)
  #:os '(EndeavourOS MacOS)
  #:languages: '((Taiwanese . thian-jiân)
                 (Chinese . 母語)
                 (English . fluent)
                 (Finnish . Osaan puhua vähän suomea)
                 (Japanese . 日本語がわからない)
                 (Deutsch . Ich kann kein Deutsch sprechen))
  #:fun-fact '(most native speakers of Chinese/Taiwanese cannot pronounce my name correctly at first))

eikyo's Issues

compile basic file

Ensure #9 works.

semantic: type check non parameteric polymorphism part

fun add(x : int, y : int) : int
  x + y

semantic: eikyo's modules

To simplify the concept, module main is preserved for the executable. Other modules all are object files, each module would be a file with a name pattern *.kyo.

# main.kyo
module main
import lib/add

fun main() : ()
  println("add(1, 2) =", add(1, 2))


# lib/add.kyo
module add
export add

fun add(a : int, b : int) : int
  a + b

As above, the import statement is followed by a path to the module. add module didn't care it's full path, but only the name of the file.

syntax: define variable

let a : int = 1
let lst : list[_] = [1, 2, 3]

_ stands for let compiler infers it.

syntax: type with mark

The current parser handles int but not int +hello, there should be able to parse them, below is the syntax:

mark ::=
  <id>
  | + <id>
  | - <id>
  | ?+ <id>
  | ?- <id>
ty ::=
  <uty> <mark>*
uty ::=
  (<<id> : <ty>>*) -> <ty>
  | <id>[<ty>+]
  | <id>

syntax: function

fun add(x : int, y : int) : int
  x + y

fun sort(xs : list[a]{+sorted}) : ()
  # ...
fun binary-search(xs : list[a]{sorted}, x : a) : bool
  # ...

the timing of the effect type really effecting the value.

Currently, our type check strategy for the timing of adding effect is pre-function, that's why we could make the ownership system. As following

fn f(x : T -owned, y : T -owned) -> ()

f(a, a)
  ^
  We would like to remove `a`'s `owned` at this place
     ^
     Then here will get the type check error

Now take into consideration if we doing the following things related to sort effect.

for instance, if we have a function f and g
with type

fn f(a : list<a> +sort, g : fn(list<a> sort) -> b) -> b

the end user could call this function with

f(a, g(a))

but the problem is when we add the effect to the value pre-function-ly, the g function passes the type check with receiving an unsorted variable a, which could cause panic, but if we are trying to do it pos-function-ly, the g will not work which is expected, but the ownership system also doesn't work.

syntax: data type

Eikyo data type is the only new type definition syntax, and struct is a syntax sugar.

type bool
  true
  false
type list[a]
  nil
  cons(a, list[a])

type person
  person{name : string, age : uint}
# <=>
struct person{name : string, age : uint}

backend: Interpreter

simplest way to check type system.

cli: `eikyo compile <app.kyo>`

Which will build a single file to binary, this part will need

1. select a CLI framework(or manually)
2. compile a file

NOTE: it can be a very simple file that like

module hello

fun main() : ()
  # ...

setup type checking in conversion checking style

syntax: macro

macro is somehow, required in Eikyo, to make sure the refinement system won't get misused.

import eikyo # import expr, block

macro when(test : expr, body : block)
  if @test
    @body

fun main() : ()
  @when true
    println("Hello, world")

Eikyo's macro is very limited

1. block must be at the end of the macro
2. @ points out it's a macro out of the macro but points out it's a macro variable in the macro
3. compiler will try to figure out macro at very beginning

backend: setup llvm

The target is simply to set up llvm-hs for a basic compiling, no need to be completely done.

backend: generate C

First, research any existing solution for a C program builder.

semantic: mark and closure

Usually, closure call or not is decided in runtime, conceptually it's compiled from

fun make-adder(n : int) : (m : int) -> int
  fun (m : int) : int
    n + m
fun main() : ()
  let f = make-adder(2)
  f(3)

to

fun make-adder(n : int) : (m : int) -> int
  fun (m : int) : int
    n + m
fun main() : ()
  let f = make-adder(2)
  if f.closure?
    f.fun(3, f.env)
  else
    f(3)

With mark

With marks in type, it's possible to find closure at compiled time

fun make-adder(n : int) : ((m : int) -> int) +closure
  fun (m : int) : int
    n + m
fun main() : ()
  # Thus, type of `f` is `((m : int) -> int) closure`
  let f = make-adder(2)
  f(3)

Eikyo compiler then knows f with closure, so compile it to

let f = make-adder(2)
f.fun(3, f.env)

semantic: mark and contract

Mark system is the biggest reason that I make Eikyo, it's a kind of tag that every type can have. For example:

mark owned

fun used-println(x : int -owned) : ()
  # NOTE: but must remember, the type of `x` is still `int owned`
  println(x)

fun main() : ()
  let a : _ +owned = 1
  used-println(a)
  # the mark owned is not hold by `a` anymore
  used-println(a) # this is not now

Another example is contract mark

contract ordered

impl ordered(xs : list[a]) : bool
  for l in xs.length()-2
    r = l+1
    if not (l <= r)
      return false
  true

fun sort(xs : list[a] +ordered) : ()
  # of course, we cannot say `xs : list[a] ordered` here
  # ...
fun binary-search(xs : list[a] ordered) : a
  # ...

In this situation, +<mark> will let compiler call the impl, and assert the result is true. At the returned place of the caller, the impl can also be thought of as an overloadable function.

For example, conceptally:

let a : list[_] = [1, 2, 3]
sort(a)
assert a.ordered()