aripiprazole / lura Goto Github PK

The current diagnostic library focus on be reliable to ariadne, the goal of this issue is using Bupropion crate for presenting errors.

• #18
• Migrate stuff that can be changed to miette from eyre
• Add a common interface between the current diagnostics and miette like a proc-macro etc
• Migrate everything to miette

https://github.com/aripiprazole/lura/blob/main/lura-typer/src/infer.rs#L1651

Currently fallsback in universe type

• #13

Constraint entailment is the satisfiability of type classes, just like the example:

In this section, we describe how class environments can be used to answer questions about which types are instances of particular classes. More generally, we consider the treatment of entailment: given a predicate p and a list of predicates ps, our goal is to determine whether p will hold whenever all of the predicates in ps are satisfied. In the special case where p = IsIn i t and ps = [], this amounts to determining whether t is an instance of the class i. In the theory of qualified types [Jones, 1992], assertions like this are captured using judgements of the form ps ||- p; we use a different notation here-the entail function that is defined at the end of this section-to make the dependence on a class environment explicit.

• Given Eq a having Ord a as superclass,
• Then Eq a satisfies Ord a

Goals

• #11
• #12

Details

• The implementation should not require explicit predicates for the entailed predicates, like
  if we have Eq a, we should not have an explicit constraint of Ord a, given the first example.

Extras

• Warns and removes all useless/unused predicates in the context

Biblio

1. https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b#entailment

https://github.com/aripiprazole/lura/blob/main/lura-typer/src/infer.rs#L1974

Refers #6, it does need #6 because we want to make let generalization with constraints, so this implementation requires let generalization being already done.

Requirements

1. #6

Details

Generalizes a function like:

Aprint : [Show a] => a -> IO ()
Bprint = Aprint

as

Aprint : [Show a] => a -> IO ()
Bprint : [Show a] => a -> IO ()
Bprint = Aprint

• Type System
  • #4
  • #5
  • #6
  • #7
  • #8
  • #9
  • Trait methods type checking
  • Class methods type checking
  • Data methods type checking
  • Mutual recursive functions on expression-level
  • Dependent types feature
• #10
  • Closure conversion
  • Coverage checking
• Resolution
  • Create class fields instead of using direct methods
  • Add an HIR indexing expression
  • Improve circular dependency error messages

• #6

https://github.com/aripiprazole/lura/blob/main/lura-typer/src/infer.rs#L1461

Creates a new abstract syntax tree containing semantic information of source code like ad-hoc,
gadt, closure conversion, etc.

Goals

• Define the THIR
• Create lower from HIR for THIR

The current implementation uses HOAS names instead of De Bruijin indexes and levels, the levels are only used in holes