Assessing using Existential Types instead of ANF

aeon/__main__.py

@@ -7,8 +7,7 @@
 from aeon.backend.evaluator import EvaluationContext
 from aeon.backend.evaluator import eval
 from aeon.core.types import top
-from aeon.decorators import Metadata
-from aeon.frontend.anf_converter import ensure_anf
+from aeon.decorators.api import Metadata
 from aeon.frontend.parser import parse_term
 from aeon.logger.logger import export_log
 from aeon.logger.logger import setup_logger
@@ -83,7 +82,7 @@ def read_file(filename: str) -> str:
         return file.read()
 
 
-def log_type_errors(errors: list[Exception | str]):
+def log_type_errors(errors: list[Exception]):
     print("TYPECHECKER", "-------------------------------")
     print("TYPECHECKER", "+     Type Checking Error     +")
     for error in errors:
@@ -92,7 +91,7 @@ def log_type_errors(errors: list[Exception | str]):
     print("TYPECHECKER", "-------------------------------")
 
 
-def main():
+def main() -> None:
     args = parse_arguments()
     logger = setup_logger()
     export_log(args.log, args.logfile, args.filename)
@@ -123,20 +122,16 @@ def main():
 
     logger.debug(core_ast)
 
-    with RecordTime("ANF conversion"):
-        core_ast_anf = ensure_anf(core_ast)
-        logger.debug(core_ast)
-
     with RecordTime("TypeChecking"):
-        type_errors = check_type_errors(typing_ctx, core_ast_anf, top)
+        type_errors = check_type_errors(typing_ctx, core_ast, top)
     if type_errors:
         log_type_errors(type_errors)
         sys.exit(1)
 
     with RecordTime("DetectSynthesis"):
         incomplete_functions: list[tuple[
-            str, list[str]]] = incomplete_functions_and_holes(
-                typing_ctx, core_ast_anf)
+            str,
+            list[str]]] = incomplete_functions_and_holes(typing_ctx, core_ast)
 
     if incomplete_functions:
         filename = args.filename if args.csv_synth else None
@@ -149,7 +144,7 @@ def main():
             synthesis_result = synthesize(
                 typing_ctx,
                 evaluation_ctx,
-                core_ast_anf,
+                core_ast,
                 incomplete_functions,
                 metadata,
                 filename,

aeon/core/instantiation.py

@@ -3,7 +3,7 @@
 from aeon.core.liquid import LiquidVar
 from aeon.core.liquid_ops import mk_liquid_and
 from aeon.core.substitutions import substitution_in_liquid
-from aeon.core.types import AbstractionType
+from aeon.core.types import AbstractionType, ExistentialType
 from aeon.core.types import BaseType
 from aeon.core.types import RefinedType
 from aeon.core.types import Type
@@ -42,6 +42,15 @@ def rec(x):
             target.kind,
             type_substitution(target.body, alpha, beta),
         )
+    elif isinstance(t, ExistentialType):
+        new_name = t.var_name
+        new_type = t.type
+        while new_name == alpha:
+            old_name = new_name
+            new_name = new_name + "_fresh"
+            new_type = type_substitution(new_type, old_name, TypeVar(new_name))
+
+        return ExistentialType(new_name, t.var_type, new_type)
     else:
         assert False
 

aeon/core/substitutions.py

@@ -18,7 +18,7 @@
 from aeon.core.terms import Rec
 from aeon.core.terms import Term
 from aeon.core.terms import Var
-from aeon.core.types import AbstractionType
+from aeon.core.types import AbstractionType, ExistentialType
 from aeon.core.types import BaseType
 from aeon.core.types import Bottom
 from aeon.core.types import RefinedType
@@ -89,29 +89,25 @@ def rec(x: Term):
     assert False
 
 
-def substitution_in_liquid(t: LiquidTerm, rep: LiquidTerm,
-                           name: str) -> LiquidTerm:
+def substitution_in_liquid(t: LiquidTerm, rep: LiquidTerm, name: str) -> LiquidTerm:
     """substitutes name in the term t with the new replacement term rep."""
     assert isinstance(rep, LiquidTerm)
-    if isinstance(t, (LiquidLiteralInt, LiquidLiteralBool, LiquidLiteralString,
-                      LiquidLiteralFloat)):
+    if isinstance(t, (LiquidLiteralInt, LiquidLiteralBool, LiquidLiteralString, LiquidLiteralFloat)):
         return t
     elif isinstance(t, LiquidVar):
         if t.name == name:
             return rep
         else:
             return t
     elif isinstance(t, LiquidApp):
-        return LiquidApp(
-            t.fun, [substitution_in_liquid(a, rep, name) for a in t.args])
+        return LiquidApp(t.fun, [substitution_in_liquid(a, rep, name) for a in t.args])
     elif isinstance(t, LiquidHole):
         if t.name == name:
             return rep
         else:
             return LiquidHole(
                 t.name,
-                [(substitution_in_liquid(a, rep, name), t)
-                 for (a, t) in t.argtypes],
+                [(substitution_in_liquid(a, rep, name), t) for (a, t) in t.argtypes],
             )
     else:
         print(t, type(t))
@@ -128,45 +124,62 @@ def rec(t: Type) -> Type:
 
     renamed: Type
 
-    if isinstance(t, Top):
-        return t
-    elif isinstance(t, Bottom):
-        return t
-    elif isinstance(t, BaseType):
-        return t
-    elif isinstance(t, TypeVar):
-        return t
-    elif isinstance(t, AbstractionType):
-        if isinstance(rep, Var) and rep.name == t.var_name:
-            nname = t.var_name + "1"
-            renamed = AbstractionType(
-                nname,
-                t.var_type,
-                substitution_in_type(t.type, Var(nname), t.var_name),
-            )
-            return substitution_in_type(renamed, rep, name)
-        elif name == t.var_name:
+    match t:
+        case Top():
             return t
-        else:
-            return AbstractionType(t.var_name, rec(t.var_type), rec(t.type))
-    elif isinstance(t, RefinedType):
-        if isinstance(rep, Var) and rep.name == t.name:
-            nname = t.name + "1"
-            renamed = RefinedType(
-                nname,
-                t.type,
-                substitution_in_liquid(t.refinement, LiquidVar(nname), t.name),
-            )
-            return substitution_in_type(renamed, rep, name)
-        elif t.name == name:
+        case Bottom():
             return t
-        else:
-            return RefinedType(
-                t.name,
-                t.type,
-                substitution_in_liquid(t.refinement, replacement, name),
-            )
-    assert False
+        case BaseType(name=_):
+            return t
+        case TypeVar(name=_):
+            return t
+        case AbstractionType(var_name=var_name, var_type=var_type, type=ity):
+            if isinstance(rep, Var) and rep.name == var_name:
+                nname = var_name + "1"
+                renamed = AbstractionType(
+                    nname,
+                    var_type,
+                    substitution_in_type(ity, Var(nname), var_name),
+                )
+                return substitution_in_type(renamed, rep, name)
+            elif name == var_name:
+                return t
+            else:
+                return AbstractionType(var_name, rec(var_type), rec(ity))
+        case RefinedType(name=ref_name, type=type, refinement=refinement):
+            # alpha renaming to avoid clashes
+            if isinstance(rep, Var) and rep.name == ref_name:
+                nname = ref_name + "1"
+                renamed = RefinedType(
+                    nname,
+                    type,
+                    substitution_in_liquid(refinement, LiquidVar(nname), ref_name),
+                )
+                return substitution_in_type(renamed, rep, name)
+            elif name == ref_name:
+                return t
+            else:
+                return RefinedType(
+                    ref_name,
+                    type,
+                    substitution_in_liquid(refinement, replacement, name),
+                )
+        case ExistentialType(var_name=var_name, var_type=var_type, type=ity):
+            # alpha renaming to avoid clashes
+            if isinstance(rep, Var) and rep.name == var_name:
+                nname = name + "1"
+                renamed = ExistentialType(
+                    nname,
+                    var_type,
+                    substitution_in_type(ity, Var(nname), var_name),
+                )
+                return substitution_in_type(renamed, rep, name)
+            if name == t.var_name:
+                return t
+            else:
+                return ExistentialType(var_name, var_type, substitution_in_type(ity, rep, name))
+        case _:
+            assert False
 
 
 def substitution(t: Term, rep: Term, name: str) -> Term:
@@ -223,16 +236,15 @@ def liquefy_app(app: Application) -> LiquidApp | None:
     elif isinstance(app.fun, Application):
         liquid_pseudo_fun = liquefy_app(app.fun)
         if liquid_pseudo_fun:
-            return LiquidApp(liquid_pseudo_fun.fun,
-                             liquid_pseudo_fun.args + [arg])
+            return LiquidApp(liquid_pseudo_fun.fun, liquid_pseudo_fun.args + [arg])
         return None
     elif isinstance(app.fun, Let):
         return liquefy_app(
             Application(
-                substitution(app.fun.body, app.fun.var_value,
-                             app.fun.var_name),
+                substitution(app.fun.body, app.fun.var_value, app.fun.var_name),
                 app.arg,
-            ), )
+            ),
+        )
     assert False
 
 

aeon/core/types.py

@@ -129,16 +129,12 @@ def __hash__(self) -> int:
         return hash(self.var_name) + hash(self.var_type) + hash(self.type)
 
 
+@dataclass
 class RefinedType(Type):
     name: str
-    type: BaseType | TypeVar
+    type: BaseType | TypeVar | Bottom | Top
     refinement: LiquidTerm
 
-    def __init__(self, name: str, ty: BaseType | TypeVar, refinement: LiquidTerm):
-        self.name = name
-        self.type = ty
-        self.refinement = refinement
-
     def __repr__(self):
         return f"{{ {self.name}:{self.type} | {self.refinement} }}"
 
@@ -154,6 +150,16 @@ def __hash__(self) -> int:
         return hash(self.name) + hash(self.type) + hash(self.refinement)
 
 
+@dataclass
+class ExistentialType(Type):
+    var_name: str
+    var_type: Type
+    type: Type
+
+    def __str__(self) -> str:
+        return f"∃{self.var_name}:{self.var_type}, {self.type}"
+
+
 @dataclass
 class TypePolymorphism(Type):
     name: str  # alpha
@@ -163,7 +169,8 @@ class TypePolymorphism(Type):
 
 def extract_parts(
     t: Type,
-) -> tuple[str, BaseType | TypeVar, LiquidTerm]:
+) -> tuple[str, BaseType | TypeVar | Top | Bottom, LiquidTerm]:
+    print(t)
     assert isinstance(t, BaseType) or isinstance(t, RefinedType) or isinstance(t, TypeVar)
     if isinstance(t, RefinedType):
         return (t.name, t.type, t.refinement)