Www pompom com how to#
Www pompom com code#

For now, we don't offer a terminating checker either positivity checker.

And yep, the design of everything can change, only for the sake of expressivity.

Thinking about the backend, We would love to target it in some practical use (like js or smart contracts).

We do want to extend the expressivity to support other higher abstractions.

I think optional constructors can extend to support computations between the patterns, if this can be possible, so deriving, for example, a quotient type using only optional constructors is probably possible (Not talking about hott here).

We are aware that our unification system implies in the k axiom, we would love to change for intensional type theory and be compatible with HOTT.

if you want to see more about this kind of stuff, follow me on twitter.You can do anything that you want to, also :).You can complete the proofs maintained on libs/chalanges and make your pull request.If you have any questions please submit it Contribute

The subtyping rules of optional constructors are something that can be detailed more with formal rules, but for now, we don't have a formal specification of it (But it's very straightforward, so no worries). The normalizer is your preference, only for the sake of simplicity is preferred to be not lazy, finally, unification is also of your preference, you could copy from the old Agda unification algorithm (you only need unification of datatype indices, do not go for circle checking or absurd., for example). Do not use the same tree in the parser and the intermediate representation.Prefer representing context as a map, instead of using type notation inside in your tree.Do not use Bruijn-index/level if you have no intention of using your implementation as a not fun tool.Implementing λΠ-calculus would be the easiest part, some not mandatory things can help in your implementation. We only made a slight modification by extending the universes, Set : Type.

Www pompom com how to#

Nevertheless, we provide a little orientation of how to do it :

Www pompom com code#

Implement it for yourselfįor now, we don't have a detailed tutorial of 'how to do it', but just studying the code and re-implementing it would be appropriated approach (and easy). You can explore more examples in libs/prelude.kei. bool_false | H :: ( Falsity ( Eq Bool true false ) ) = > def Bool→ * = | b :: ~ Bool ~ > * => ( eq_rect Bool true false Bool→ * H I ). A false is also a Unit type, but it don't have a constructor, it is the same that forall (x : True), x I in Coq for example Falsity | A :: ~ * ~ > Type => ~ A ~ > False. data List a = | New a (List a) | Empty List | A :: ~ * ~ > * =>.