dannypsnl / eikyo

polymorphsim language with mark system

eikyo(影响)

eikyo is an experimental programming language, exploring a mark system with usual polymorphic type, I will try to explain the idea informally in the following section.

Polymorphic type means parameteric polymorphism here. For each type, they can have a set of marks. For example, int positive is a type int with a mark positive. A mark can be operated, for example, the following code shows a ownership system.

fun use(t : T -owned) : ()
  # ...

fun main() : ()
  let t : T +owned = # ...
  use(t)
  use(t) # error: t is not owned

The reason that works, is because -mark is saying that I expected the argument has that mark, and will don't have that mark at caller environment after position get evaluated. This is important, because we might also write the following.

fun use1(a : A -owned) : B
  # ...

fun use2(a : A -owned, b : B -owned) : ()
  # ...

fun main() : ()
  let t : T +owned = # ...
  use2(t, use1(t)) # error: t is not owned at `use1`

This example shows the type of t get affected exactly at the position use2(t, ...) evaluated. Another part is +owned, the semantic of this is adding mark to the type if don't have.

A mark can associate with a contract, for example, we can have below code.

contract positive(n : int) : bool
  n > 0

fun main() : ()
  let a : int +positive = 1

The code will be expanded to

fun positive(n : int) : bool
  n > 0

fun main() : ()
  let a : int = 1
  @assert a.positive()

Thus, we can make sure the mark is correct, because the runtime will block invalid code.

All mark operations are

• +
• -
• ?+
• ?-
• require, when we didn't write any operation with mark, it requires the mark exists.

Plan

1. A full compiler from source code to generated code, now having some problems
   • llvm-hs has problem with brew installed llvm@12

Invite

We invite developers to participate, please contact ([email protected]) if you have any questions. A description of the semantics and syntax is developing. Due to the semantics and development content, there may be many unclear or undefined matters in the issue, and you are welcome to provide valuable comments.

Developers are expected to be proficient in FP(e.g. Haskell, Racket, SML) and able to develop independently in at least one of the following situations

1. parser: we use megaparsec, a parser combinator
2. type system: based on Hindley-Milner, with additional "mark" system
3. macro system: macro based on syntax tree modification
4. llvm: some understanding of coding higher-order abstractions with llvm
5. package system: good experience in implementation, able to design or maintain system for package upload, installation, and compilation
6. standard library: interested in learning new languages and writing high-quality programs

Hope this note has really given you an idea of what you can contribute.

The principle of an issue is that it can be completed within a week (bug related is not limited to this) If it cannot be completed within this time, which means that it is not clearly achievable, it will be referred to https://github.com/dannypsnl/eikyo/discussions. It's okay to open the wrong issue, the maintainer will let you know and move the content to the relevant location for you.

eikyo's Issues

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

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.

setup type checking in conversion checking style

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
  # ...

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}

compile basic file

Ensure #9 works.

backend: Interpreter

simplest way to check type system.

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.

semantic: type check non parameteric polymorphism part

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

backend: generate C

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

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() : ()
  # ...

backend: setup llvm

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

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()

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>