Currently, the Typechecker monad has a rigid order and set of constraints.
We should convert it to a set of Eff member constraint and keep the underlying monad polymorphic

Assignees: @tiansivive
Labels: Effects, enhancement
Milestone:

https://github.com/tiansivive/saga/blob/cc4e21b3fe78af8491ed42515b89cf95c040fe2f/src/Saga/Language/Typechecker/Solver/Monad.hs#L35

Discussed in #38

Proposed syntax:

let comprehension 
    = \xs -> yield (x + y) from {
      x <- xs if isEven |> (>5) 
      y <- range 0 x

      then take 5
      then group by y
    } using someMonadImpl

We take advantage of curly blocks to introduce then constructs, similar to haskell list comprehensions

We add if clauses (potentially unless too) to backcall, which get desugared to guards on the results of the backcall

Questions:
Do we need to ensure purity? Do we need to work only with monads?

A then statements could simply desugar to introducing a new code block scoped to all the variables of the current block.
For example:

yield (x + y) from {
  x <- xs
  y <- range 0 x

  then take 5
}

Would desugar to:

yield (x + y) from {
  return take 5 {
     x <- xs
     y <- range 0 x
     return (x,y)
  }
}

Consequently, one can do

yield (x + y) from {
  x <- xs
  y <- range 0 x

  (x', y') <- then take 5

  return (x' +1, y' +1)
}

Which desugars to

yield (x + y) from {
  (x', y') <- take 5 {
     x <- xs
     y <- range 0 x
     return (x,y)
  }
  return (x' +1, y' +1)
}

This is how to identify that a certain type has been refined/narrowed. We can create a new type of evidence that gets stored in the environment, and can be looked up in order to understand if a type has been refined

Assignees: @tiansivive
Labels: Liquids, Constraint Solver,Typechecker
Milestone: Liquid Types

Ref: #23

Assignees: @tiansivive
Labels: Effects, Entailment, enhancement
Milestone:

https://github.com/tiansivive/saga/blob/cc4e21b3fe78af8491ed42515b89cf95c040fe2f/src/Saga/Language/Typechecker/Solver/Entailment.hs#L22

Improve type subtype narrowing by resolving variance issues.

For example, in the expressions:

match x
  |  1    -> return x 
  |  "Hi" -> return x

Do we want to infer x as Int | String or 1 | "Hi"?
Similarly, do we keep subtypes in the match expression return type?

An option would be to preserve subtypes when no catch-all case is provided, which would be in line with totality/exhaustiveness, and generalize to supertypes (Int | String) when catch-all/default cases exist

Add a variadic param type, inspired by Typescript's rest params

Possible syntax:

fn: Int -> ...String -> Bool



> fn 1!         -- FnApp <fn> [TLit 1, TVariadic []]
> fn 1 "hello"! -- FnApp <fn> [TLit 1, TVariadic [TLit "hello"]]

Edge cases:

fn: ...String -> String -> Int


> fn "hello"!         -- FnApp <fn> [ TVariadic [], TLit "hello"]
> fn "hello" "world"! -- FnApp <fn> [ TVariadic [TLit "hello"], TLit "world"]

Currently, inference generalizes types too early, during the initial AST traversal and constraint generation phase.
Propose moving generalization to after the solver has finished. This would prevent losing narrowed type information, crucial for refinements, which is currently broken.

• Infer values as Pure by default
• Default blocks to impure, unless they preserve purity via using clauses.
• Investigate adding Purity constraints to type bindings and whether that overrules impure inference rules

Currently evaluating/inferring type lambdas adds the param bindings to the global type vars environment.
What's needed is a similar approach to term level lambda evaluation, where we have a closure'd env, ie. a "Scope"!

Main use would be in the Substitution typeclass, but could perhaps be extended to:
* PolymorphicVar
* Inference: Perhaps removing the need for Classifier family
* Generalization & Instantiation
* Type Evaluation

Assignees: @tiansivive
Labels: Substituions, enhancement, Unification, Constraint Solver,
Milestone:

https://github.com/tiansivive/saga/blob/cc4e21b3fe78af8491ed42515b89cf95c040fe2f/src/Saga/Language/Typechecker/Solver/Substitution.hs#L14

Singleton types are essentially subtypes of the Int, Bool and String primitive types. That causes inconsistencies dueing inference, especially for liquids, as we want to keep the most specific (the Singleton) type for refinements, and yet have it unify as the more general primitve.
To solve this, we should investigate also generating "proofs/witenesses" when dealing with singleton types, probably during unification, when binding to a type variable.

TConstructor vs TParametric vs TClosure

Need to remove the indecision regarding parametric types.
Currently, the notation MyType<Int> parses into TParametric, with the latter taking an array of the type arguments.

Instead, we should take advantage of Type Function Application expressions and enforce the following syntax:

MyType Int!

MyType would be be defined as:

//potentially allow/require `forall` annotation
type MyType = \a -> { value: a } // or whatever other output type.

and would be parsed as a TypeExpression. Evaluating this tyExpr will then result in a TParametric

eval (TLambda args body) = TParametric <first arg> <output type | recursive TParametric>

This enforces type arg currying and takes advantage of the same semantics as term level expressions and evaluation.

Preference for TParametric over TConstructor to not cause confusion with type constructors as defined by data declarations like:

data Maybe = \a -> Just: a | Nothing

This was a hack to prevent cycling dependencies issues.
https://github.com/tiansivive/saga/blob/77d413fcce31567fc8e5df63a6e1f5fd97f075c1/src/Saga/Language/Typechecker/Solver/Run.hs#L163

Check both protocol declaration and implementations

Assignees: @tiansivive
Labels: Entailment, enhancement
Milestone:

https://github.com/tiansivive/saga/blob/cc4e21b3fe78af8491ed42515b89cf95c040fe2f/src/Saga/Language/Typechecker/Solver/Protocols.hs#L69

Right now, if both refinements and evidence implement an instance of Restricted, then a refinement var could be used where an evidence var is expected, and vice-versa

• SUGGESTION: More type families - one for each.
• SUGGESTION: One more elaborate type family: Context
• QUESTION: How to implement a Context type family?

Assignees: @tiansivive,
Labels: Variables,bug enhancement, Typechecker, Constraint Solver, question,
Milestone:

https://github.com/tiansivive/saga/blob/cc4e21b3fe78af8491ed42515b89cf95c040fe2f/src/Saga/Language/Typechecker/Variables.hs#L40

Steps required:

• parsing
• inference
• namespacing tags
• elaboration
• generation

** Liquid types **

Right now, we can parse something like

type Foo = a 
  where 
    a = Int,
    a | \x => 1 

Which is not very useful because we can't do arbitrary conditions.

Ideally we want to express refinements like

a | \x => x > 0

By taking advantage of type unions, we can introduce function overloading.

This can be useful for having different APIs, for example, curried vs uncurried versions or different parameter order for readability purposes

Use TS inspired Bidirectional type checking, using HM for the inference/synthesis part