Aladdin Proposals
KiJeong-Lim opened this issue · 1 comments
KiJeong-Lim commented
- Introduce module system.
- Introduce Haskell's feature (
data
rather thankind
, type synonym, type class). - Make error messages pretty.
- Allow
D ::= D /\ D
. - Allow user-defined operators.
- Introduce constraint handling rules (CHR) like Elpi.
KiJeong-Lim commented
-
CHR:
<Goal> ::= <Var> "with" <Goal>
G with P
successes iffX
is a logic variable.
ifX with P
successes then yields constraintP
forX
. -
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).