Aladdin Proposals

[KiJeong-Lim]

1. Introduce module system.
2. Introduce Haskell's feature (data rather than kind, type synonym, type class).
3. Make error messages pretty.
4. Allow D ::= D /\ D.
5. Allow user-defined operators.
6. Introduce constraint handling rules (CHR) like Elpi.

[KiJeong-Lim]

1. CHR:
   <Goal> ::= <Var> "with" <Goal>
G with P successes iff X is a logic variable.
   if X with P successes then yields constraint P for X.

2. Meta Aladdin:

module TC.

from Std import Aladdin.MetaAladdin as MA.

data ty : * where
  all : (ty -> ty) -> ty.
  arr : ty -> ty -> ty.

data tm : * where
  abs : (tm -> tm) -> tm.
  app : tm -> tm -> tm.
  let : tm -> (tm -> tm) -> tm.

check (let Rhs Body) Tau :-
  MA.runMeta (MA.mkNewVar (Sigma0\ MA.solve (check Rhs Sigma0) (Res Sigma0))),
  -- Res := Sigma0\ sigma (Alpha_1\ ... sigma (Alpha_n\ Sigma = Gen Alpha_1 ... Alpha_n)) for some skeleton Gen 
  generalize (Res _) Scheme,
  -- Scheme := all (Alpha_1\ ... all (Alpha_n\ Gen Alpha_1 ... Alpha_n))
  pi (X\ check X Scheme => check (Body X) Tau).