owo-lang / voile-rs Goto Github PK

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

Currently, the desugar functions have too many repetitive parameters:

• env
• global_map
• local_env
• local_map

Consider putting them together.

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

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

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.

We can replace VecDbiEnv with a Vec.

These codes are affected:

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

Useful for REPLs

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.

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.

According to @molikto

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

#16 depends on this.

Should be possible after #77

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

Which are bottom-eliminator and pattern matching fallbacker.

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.

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

Because I feel like it's rather important

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

Created by @ice1000 from Gitter

Remove these things:

• TCS::compile
• eval::Strategy

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

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.

As title

But we can replace DbiEnv with Vec

Originally posted by @ice1000 in #15 (comment)

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

Originally posted by @ice1000 in #38

.. and Pi/Sigma should keep

s/dtlac/dtalc/g

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

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?

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

As described by @uHOOCCOOHu

As title.

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

Currently it panics when level check failed

Let's test lambda translation

Originally posted by @ice1000 in #44 (comment)