Currently it panics when level check failed

Remove these things:

• TCS::compile
• eval::Strategy

Use use abs::Abs::* in check::check_type.

This is intended to be a discussion thread about focuses of Voile.

There is also a bikeshedding here: do we need to change the org name to owo-lab for storing these kinds of PoC languages?

First of all, \x.\y.y is Lam(Lam(Dbi(0)).
Instantiate this (e.g. with a value 114514), according to our current strategy, will produce Lam(114514), which means that our implementation is evaluating (\x.\y.y) 114514 to \y.114514.

Junk! Need to fix it asap.

Due to the presence of Abs, we won't be able to resolve implicit parameters when translating String-based variables to DBI, thus giving up implicit parameters.

... and we need to invent a way to merge two SyntaxInfos

As title

Because we're already splitting the local and global typing context, should we split the value context as well?

But we can replace DbiEnv with Vec

Originally posted by @ice1000 in #15 (comment)

And I'm looking for a better name for the function

DBI-based lambda does not need a capturing list and it should always be lifted during instantiation. Current lambda instantiation is completely wrong.

Originally posted by @ice1000 in #16 (comment)

This is a subtask of #16

.. and Pi/Sigma should keep

We can replace VecDbiEnv with a Vec.

These codes are affected:

after all these we can start testing our trans/check functions

As title.

Which are bottom-eliminator and pattern matching fallbacker.

We may need a parser that produces well-typed terms for testing purpose.

#16 depends on this.

As described by @uHOOCCOOHu

s/dtlac/dtalc/g

Useful for REPLs

Currently there's only a label -- without a type expression that represents its argument type.

If I write an expression 'Label ParamType, it'll be parsed as App(ConsType(Label), Expr(Ident)),
which indicates that the type of 'Label is Lam(Type /* param type */, Sum(Ref(0 /* DBI */))), right?

Does that look good to you guys?

Assigned people are supposed to participate the discussion.

Should be possible after #77

Because an axiom can be unimplemented (recursive-calls) or postulated. There can be many kinds of axioms.

Extracting a standalone type will also be helpful for map_axioms.

We need a way to compile abs to core without typechecking.

This is useful when we can successfully infer the type of some expressions but we also need their values. These expressions are supposed to be well-typed thus can be unsafe-compile.

According to @molikto

Meow~
This pull-request is created automatically by @owo-bot.

Created by @ice1000 from Gitter

What is this SyntaxInfo? Parameter syntax info or the whole lambda?
Do we need two SyntaxInfos?

Originally posted by @ice1000 in #38

Or I may need to write a translator from Axi-based core terms to Var-based

Because I feel like it's rather important

Currently, we have already got DBI in our abstract syntax.
This is causing problems -- type checking against DBI-based lambdas is difficult.

I want to redesign the abstract syntax according to MiniAgda, which have a similar architecture of Voile (Concrete (syntax-checked), Abstract (scope-checked), Value (type-checked)) but does not use DBI in abstract. Instead, it uses DBI in values but UIDs in abstract.

https://www.microsoft.com/en-us/research/wp-content/uploads/1999/01/recpro.pdf
https://github.com/willtim/row-polymorphism/blob/master/src/AlgorithmW_ConstrainedRows.hs

Currently, the desugar functions have too many repetitive parameters:

• env
• global_map
• local_env
• local_map

Consider putting them together.

Or is my DBI context is cumulative so I don't need to lift anything?
Dunno, need to test it.

Let's vote.

Option 0 (Haskell, add a 🎉 to vote for this):

\x -> x
\x y -> y x

Option 1 (Idris, add a 🚀 to vote for this):

\x => y
\x => \y => y x

Option 2 (Mini-TT, add a ❤️ to vote for this):

\x. x
\x y. y x

BTW we need to improve the "type check successful" message according to Voile herself:

Let's test lambda translation

Originally posted by @ice1000 in #44 (comment)