eashanhatti / peridot Goto Github PK

Getting my thought process for the design of the staging system down:

Staging allows us to express in the type system when a computation will take place. Implementing this is pretty simple, we index Type by a term of type Stage, which can be either 0 for run time or 1 for compile time (arbitrary names). Terms of kind Type 0 are evaluated at run time, while terms of kind Type 1 are evaluated at compile time.

if True : Bool : Type 0 then 33 else 34 -- run time `if`, eliminates a run time `Bool`
if True : Bool : Type 1 then 33 else 34 -- compile time `if`, eliminates a compile time `Bool`

However, we already run into a problem with this system, what if we make a stage of kind Type 0 - a stage evaluated at run time?

id : (s : Stage : Type 0) -> (A : Type s) -> A -> A
id _ _ x = x

id 1 String "foo"

This example doesn't make sense. "foo" is evaluated at compile time, hence the 1 passed to id, but the 1 is evaluated at run time. It will only be known at run time that "foo" should be evaluated at compile time. A fix that seems to work at first is just disallowing stages of kind Type 0:

id : (s : Stage : Type 1) -> (A : Type s) -> A -> A
id _ _ x = x

id 1 String "foo"

The s : Stage : Type 0 has been changed to s : Stage : Type 1. However, this actually doesn't work either. The 1 will be evaluated at compile time, but it will still be passed to id at run time. This narrows down the problem a bit: The problem is not that stages can be evaluated at run time, but rather that they can exist at run time at all. All that's need is for stages to be erased. Erasure it turns out, can be implemented in terms of the staging system. What we do is add another stage, let's call it 2, for terms that are evaluated at compile time and cannot be contained inside of a term that is not of stage 2. For pi types, if either the input or output types are stage 2, the pi type itself must be of stage 2. The same is true for sigma types and their components. The above example is now an ill-typed program as we need it to be, we have to write it like this (note that the Type 2 annotation on the function type is for clarity here, it could be inferred):

id : ((s : Stage : Type 2) -> (A : Type s) -> A -> A) : Type 2
id _ _ x = x

id 1 String "foo"

The function taking s as well as the argument passed for s will be evaluated at compile time, leaving a function of type (A : Type 1) -> A -> A for run time.

Considering memory management options at the moment.
On the table:

• Tracing GC
• RC

Off the table:

• Regions. Region inference becomes woefully imprecise in the presence of lazy evaluation, which Konna will use.

I'm thinking that we'll use a combination of RC and GC. The only strict limitation RC has is that it can't deal with cycles. So we can have two kinds of datatypes - strictly positive ones and ones without that restriction. The former can be managed by RC optimized along the lines of Lobster. The latter can be collected by a tracing GC.

I tried to build and got a linker error in building konna_editor.

There's no build instructions to follow, so I'll describe what I did.

I created a stack.yaml file:

packages:
- '.'
resolver: lts-18.20
allow-newer: true
extra-deps:
- fused-effects-1.1.1.1@sha256:c029c5fb0b2154281221a71ff25709d2a11347fe061fa8c2398e7fe52a16008d,4932
- syz-0.2.0.0@sha256:7307acb8f6ae7720e7e235c974281ecee912703c1394ebcac19caf83d70bb492,2345

(note that the extra-deps section is verbatim what stack suggests adding when it fails without them)

Then I run

% stack test
...
WARNING: Ignoring konna's bounds on base (>=4.15.0.0 && <4.16); using base-4.14.3.0.
Reason: allow-newer enabled.
base-compat                > using precompiled package
base-orphans               > using precompiled package
...
[12 of 12] Compiling Main
Linking .stack-work/dist/x86_64-osx/Cabal-3.2.1.0/build/konna_compiler/konna_compiler ...
Preprocessing executable 'konna_editor' for konna-0.1.0.0..
Building executable 'konna_editor' for konna-0.1.0.0..
[ 1 of 12] Compiling Elaboration.Error[boot]
[ 2 of 12] Compiling Etc
[ 3 of 12] Compiling Norm[boot]
[ 4 of 12] Compiling Surface
[ 5 of 12] Compiling Parsing
[ 6 of 12] Compiling Var
[ 7 of 12] Compiling Core
[ 8 of 12] Compiling Norm
[ 9 of 12] Compiling Unification
[10 of 12] Compiling Elaboration.Error
[11 of 12] Compiling Elaboration
[12 of 12] Compiling Main
Linking .stack-work/dist/x86_64-osx/Cabal-3.2.1.0/build/konna_editor/konna_editor ...
Undefined symbols for architecture x86_64:
  "_getch", referenced from:
      _Lc2tK3_info in Main.o
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
`gcc' failed in phase `Linker'. (Exit code: 1)
                     
Warning: There were multiple candidates for the Cabal entry Main.hs 
         * /Users/yairchu/dev/src/konna/editor/Main.hs
         * /Users/yairchu/dev/src/konna/compiler/Main.hs 
         picking: /Users/yairchu/dev/src/konna/editor/Main.hs
Completed 27 action(s).

--  While building package konna-0.1.0.0 (scroll up to its section to see the error) using:
      /Users/yairchu/.stack/setup-exe-cache/x86_64-osx/Cabal-simple_mPHDZzAJ_3.2.1.0_ghc-8.10.7 --builddir=.stack-work/dist/x86_64-osx/Cabal-3.2.1.0 build exe:konna_compiler exe:konna_editor --ghc-options " -fdiagnostics-color=always"
    Process exited with code: ExitFailure 1

Running on macOS 12.1 on an M1 MacBook Pro using stack v2.7.3.