Notes

TODO.md

@@ -22,3 +22,25 @@
 - Try to implement the min and max functions using select
 
 - Read https://bytecodealliance.org/articles/multi-value-all-the-wasm
+
+
+- GRose :: (* -> *) -> * -> *
+- skolem => variable that cannot be unified
+
+
+Limitations (for now):
+- no type level nats
+- only support first order kinds
+  Do not support yet:
+  ```
+  data Record f = Record {
+    field: f Int
+  }
+  Record :: (* -> *) -> *
+  ```
+  (Nested arrows)
+- only support rank 1 types
+  ```
+  mapRecord :: forall f g. (forall a. f a -> f b) -> Record f -> Record g
+  ```
+  (Nested forall)

phasm/build/base.py

@@ -27,6 +27,7 @@ from ..type3.types import (
     TypeConstructor_Struct,
     TypeConstructor_Tuple,
 )
+from ..type5.typeexpr import TypeExpr as Type5Expr
 from ..wasm import WasmType, WasmTypeInt32, WasmTypeNone
 from . import builtins
 
@@ -67,6 +68,7 @@ class BuildBase[G]:
         'type_info_constructed',
 
         'types',
+        'type5s',
         'type_classes',
         'type_class_instances',
         'type_class_instance_methods',
@@ -142,6 +144,11 @@ class BuildBase[G]:
     Types that are available without explicit import.
     """
 
+    type5s: dict[str, Type5Expr]
+    """
+    Types that are available without explicit import.
+    """
+
     type_classes: dict[str, Type3Class]
     """
     Type classes that are available without explicit import.
@@ -193,6 +200,7 @@ class BuildBase[G]:
             'None': self.none_,
             'bool': self.bool_,
         }
+        self.type5s = {}
         self.type_classes = {}
         self.type_class_instances = set()
         self.type_class_instance_methods = {}

phasm/build/builtins.py

@@ -14,6 +14,8 @@ from ..type3.types import (
     TypeConstructor_Struct,
     TypeConstructor_Tuple,
 )
+from ..type5.kindexpr import Star
+from ..type5.typeexpr import TypeConstructor as Type5Constructor
 
 dynamic_array = TypeConstructor_DynamicArray('dynamic_array')
 function = TypeConstructor_Function('function')
@@ -24,3 +26,6 @@ tuple_ = TypeConstructor_Tuple('tuple')
 bool_ = Type3('bool', TypeApplication_Nullary(None, None))
 none_ = Type3('None', TypeApplication_Nullary(None, None))
 
+s = Star()
+
+static_array5 = Type5Constructor(name="static_array", kind=s >> s)

phasm/build/default.py

@@ -11,6 +11,7 @@ from ..type3.types import (
     Type3,
     TypeApplication_Nullary,
 )
+from ..type5 import typeexpr as type5typeexpr
 from ..wasm import (
     WasmTypeFloat32,
     WasmTypeFloat64,
@@ -82,6 +83,10 @@ class BuildDefault(BuildBase[Generator]):
             'bytes': bytes_,
         })
 
+        self.type5s.update({
+            'u8': type5typeexpr.AtomicType('u8')
+        })
+
         tc_list = [
             bits,
             eq, ord,

phasm/ourlang.py

@@ -7,18 +7,21 @@ from .build.base import BuildBase
 from .type3.functions import FunctionSignature, TypeVariableContext
 from .type3.typeclasses import Type3ClassMethod
 from .type3.types import Type3, TypeApplication_Struct
+from .type5 import typeexpr as type5typeexpr
 
 
 class Expression:
     """
     An expression within a statement
     """
-    __slots__ = ('type3', )
+    __slots__ = ('type3', 'type5', )
 
     type3: Type3 | None
+    type5: type5typeexpr.TypeExpr | None
 
     def __init__(self) -> None:
         self.type3 = None
+        self.type5 = None
 
 class Constant(Expression):
     """
@@ -339,17 +342,19 @@ class ModuleConstantDef:
     """
     A constant definition within a module
     """
-    __slots__ = ('name', 'lineno', 'type3', 'constant', )
+    __slots__ = ('name', 'lineno', 'type3', 'type5', 'constant', )
 
     name: str
     lineno: int
     type3: Type3
+    type5: type5typeexpr.TypeExpr
     constant: Constant
 
-    def __init__(self, name: str, lineno: int, type3: Type3, constant: Constant) -> None:
+    def __init__(self, name: str, lineno: int, type3: Type3, type5: type5typeexpr.TypeExpr, constant: Constant) -> None:
         self.name = name
         self.lineno = lineno
         self.type3 = type3
+        self.type5 = type5
         self.constant = constant
 
 class ModuleDataBlock:
@@ -383,11 +388,12 @@ class Module[G]:
     """
     A module is a file and consists of functions
     """
-    __slots__ = ('build', 'data', 'types',  'struct_definitions', 'constant_defs', 'functions', 'methods', 'operators', 'functions_table', )
+    __slots__ = ('build', 'data', 'types', 'type5s', 'struct_definitions', 'constant_defs', 'functions', 'methods', 'operators', 'functions_table', )
 
     build: BuildBase[G]
     data: ModuleData
     types: dict[str, Type3]
+    type5s: dict[str, type5typeexpr.TypeExpr]
     struct_definitions: Dict[str, StructDefinition]
     constant_defs: Dict[str, ModuleConstantDef]
     functions: Dict[str, Function]
@@ -400,6 +406,7 @@ class Module[G]:
 
         self.data = ModuleData()
         self.types = {}
+        self.type5s = {}
         self.struct_definitions = {}
         self.constant_defs = {}
         self.functions = {}

phasm/parser.py

@@ -34,6 +34,7 @@ from .ourlang import (
 )
 from .type3.typeclasses import Type3ClassMethod
 from .type3.types import IntType3, Type3
+from .type5 import typeexpr as type5typeexpr
 from .wasmgenerator import Generator
 
 
@@ -101,6 +102,7 @@ class OurVisitor[G]:
         module.methods.update(self.build.methods)
         module.operators.update(self.build.operators)
         module.types.update(self.build.types)
+        module.type5s.update(self.build.type5s)
 
         _not_implemented(not node.type_ignores, 'Module.type_ignores')
 
@@ -264,6 +266,7 @@ class OurVisitor[G]:
                 node.target.id,
                 node.lineno,
                 self.visit_type(module, node.annotation),
+                self.visit_type5(module, node.annotation),
                 value_data,
             )
 
@@ -277,6 +280,7 @@ class OurVisitor[G]:
                 node.target.id,
                 node.lineno,
                 self.visit_type(module, node.annotation),
+                self.visit_type5(module, node.annotation),
                 value_data,
             )
 
@@ -290,6 +294,7 @@ class OurVisitor[G]:
                 node.target.id,
                 node.lineno,
                 self.visit_type(module, node.annotation),
+                self.visit_type5(module, node.annotation),
                 value_data,
             )
 
@@ -664,6 +669,18 @@ class OurVisitor[G]:
 
         raise NotImplementedError(f'{node} as type')
 
+    def visit_type5(self, module: Module[G], node: ast.expr) -> type5typeexpr.TypeExpr:
+        if isinstance(node, ast.Name):
+            if not isinstance(node.ctx, ast.Load):
+                _raise_static_error(node, 'Must be load context')
+
+            if node.id in module.type5s:
+                return module.type5s[node.id]
+
+            _raise_static_error(node, f'Unrecognized type {node.id}')
+
+        raise NotImplementedError
+
 def _not_implemented(check: Any, msg: str) -> None:
     if not check:
         raise NotImplementedError(msg)

phasm/type4/classes.py

@@ -0,0 +1,131 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import TypeAlias
+
+## Kind * (part 1)
+
+@dataclass
+class Atomic:
+    """
+    Atomic (or base or fundamental) type - it doesn't construct anything and wasn't constructed
+    """
+    name: str
+
+class Struct(Atomic):
+    """
+    Structs are a fundamental type. But we need to store some extra info.
+    """
+    fields: list[tuple[str, Type4]]
+
+@dataclass
+class Variable:
+    """
+    Type variable of kind *.
+    """
+    name: str
+
+@dataclass
+class Nat:
+    """
+    Some type constructors take a natural number as argument, rather than a type.
+    """
+    value: int
+
+    @property
+    def name(self) -> str:
+        return str(self.value)
+
+## Kind * -> *
+
+@dataclass
+class ConcreteConSS:
+    """
+    An concrete type construtor of kind * -> *, like dynamic array.
+    """
+    name: str
+
+@dataclass
+class VariableConSS:
+    """
+    A type variable of kind * -> *.
+    """
+    name: str
+
+@dataclass
+class AppliedConSS:
+    """
+    An application of a type constructor of kind * -> *.
+
+    The result is a type of kind *.
+    """
+    con: ConcreteConSS | VariableConSS | AppliedConSSS | AppliedConNSS
+    arg: Type4
+
+    @property
+    def name(self) -> str:
+        return f'{self.con.name} {self.arg.name}'
+
+## Kind * -> * -> *
+
+@dataclass
+class ConcreteConSSS:
+    """
+    An concrete type construtor of kind * -> * -> *, like function, tuple or Either.
+    """
+    name: str
+
+@dataclass
+class VariableConSSS:
+    """
+    A type variable of kind * -> * -> *.
+    """
+    name: str
+
+@dataclass
+class AppliedConSSS:
+    """
+    An application of a type constructor of kind * -> * -> *.
+
+    The result is a type construtor of kind * -> *.
+    """
+    con: ConcreteConSSS | VariableConSSS
+    arg: Type4
+
+    @property
+    def name(self) -> str:
+        return f'{self.con.name} {self.arg.name}'
+
+## Kind Nat -> * -> *
+
+@dataclass
+class ConcreteConNSS:
+    """
+    An concrete type construtor of kind Nat -> * -> *, like static array.
+    """
+    name: str
+
+@dataclass
+class VariableConNSS:
+    """
+    A type variable of kind Nat -> * -> *.
+    """
+    name: str
+
+@dataclass
+class AppliedConNSS:
+    """
+    An application of a type constructor of kind Nat -> * -> *.
+
+    The result is a type construtor of kind * -> *.
+    """
+    con: ConcreteConNSS | VariableConNSS
+    arg: Nat
+
+    @property
+    def name(self) -> str:
+        return f'{self.con.name} {self.arg.name}'
+
+# Kind * (part 2)
+
+Type4: TypeAlias = Atomic | Variable | AppliedConSS

phasm/type4/unify.py

@@ -0,0 +1,202 @@
+from dataclasses import dataclass
+
+from .classes import (
+    AppliedConNSS,
+    AppliedConSS,
+    AppliedConSSS,
+    Atomic,
+    ConcreteConNSS,
+    ConcreteConSS,
+    ConcreteConSSS,
+    Type4,
+    Variable,
+    VariableConNSS,
+    VariableConSS,
+    VariableConSSS,
+)
+
+
+@dataclass
+class Failure:
+    """
+    Both types are already different - cannot be unified.
+    """
+    msg: str
+
+@dataclass
+class Action:
+    pass
+
+UnifyResult = Failure | list[Action]
+
+@dataclass
+class SetTypeForVariable(Action):
+    var: Variable
+    type: Atomic | AppliedConSS
+
+@dataclass
+class SetTypeForConSSVariable(Action):
+    var: VariableConSS
+    type: ConcreteConSS | AppliedConSSS | AppliedConNSS
+
+@dataclass
+class SetTypeForConSSSVariable(Action):
+    var: VariableConSSS
+    type: ConcreteConSSS
+
+@dataclass
+class ReplaceVariable(Action):
+    before: Variable
+    after: Variable
+
+@dataclass
+class ReplaceConSSVariable(Action):
+    before: VariableConSS
+    after: VariableConSS
+
+def unify(lft: Type4, rgt: Type4) -> UnifyResult:
+    """
+    Tries to unify the given two types.
+    """
+    if isinstance(lft, Atomic) and isinstance(rgt, Atomic):
+        if lft == rgt:
+            return []
+
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, Atomic) and isinstance(rgt, Variable):
+        return [SetTypeForVariable(rgt, lft)]
+
+    if isinstance(lft, Atomic) and isinstance(rgt, AppliedConSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, Variable) and isinstance(rgt, Atomic):
+        return [SetTypeForVariable(lft, rgt)]
+
+    if isinstance(lft, Variable) and isinstance(rgt, Variable):
+        return [ReplaceVariable(lft, rgt)]
+
+    if isinstance(lft, Variable) and isinstance(rgt, AppliedConSS):
+        return [SetTypeForVariable(lft, rgt)]
+
+    if isinstance(lft, AppliedConSS) and isinstance(rgt, Atomic):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConSS) and isinstance(rgt, Variable):
+        return [SetTypeForVariable(rgt, lft)]
+
+    if isinstance(lft, AppliedConSS) and isinstance(rgt, AppliedConSS):
+        con_res = unify_con_ss(lft.con, rgt.con)
+        if isinstance(con_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        arg_res = unify(lft.arg, rgt.arg)
+        if isinstance(arg_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        return con_res + arg_res
+
+    raise NotImplementedError
+
+def unify_con_ss(
+        lft: ConcreteConSS | VariableConSS | AppliedConSSS | AppliedConNSS,
+        rgt: ConcreteConSS | VariableConSS | AppliedConSSS | AppliedConNSS,
+    ) -> UnifyResult:
+    """
+    Tries to unify the given two constuctors of kind * -> *.
+    """
+    if isinstance(lft, ConcreteConSS) and isinstance(rgt, ConcreteConSS):
+        if lft == rgt:
+            return []
+
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, ConcreteConSS) and isinstance(rgt, VariableConSS):
+        return [SetTypeForConSSVariable(rgt, lft)]
+
+    if isinstance(lft, ConcreteConSS) and isinstance(rgt, AppliedConSSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, ConcreteConSS) and isinstance(rgt, AppliedConNSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, VariableConSS) and isinstance(rgt, ConcreteConSS):
+        return [SetTypeForConSSVariable(lft, rgt)]
+
+    if isinstance(lft, VariableConSS) and isinstance(rgt, VariableConSS):
+        return [ReplaceConSSVariable(lft, rgt)]
+
+    if isinstance(lft, VariableConSS) and isinstance(rgt, AppliedConSSS):
+        return [SetTypeForConSSVariable(lft, rgt)]
+
+    if isinstance(lft, VariableConSS) and isinstance(rgt, AppliedConNSS):
+        return [SetTypeForConSSVariable(lft, rgt)]
+
+    if isinstance(lft, AppliedConSSS) and isinstance(rgt, ConcreteConSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConSSS) and isinstance(rgt, VariableConSS):
+        return [SetTypeForConSSVariable(rgt, lft)]
+
+    if isinstance(lft, AppliedConSSS) and isinstance(rgt, AppliedConSSS):
+        con_res = unify_con_sss(lft.con, rgt.con)
+        if isinstance(con_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        arg_res = unify(lft.arg, rgt.arg)
+        if isinstance(arg_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        return con_res + arg_res
+
+    if isinstance(lft, AppliedConSSS) and isinstance(rgt, AppliedConNSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConNSS) and isinstance(rgt, ConcreteConSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConNSS) and isinstance(rgt, VariableConSS):
+        return [SetTypeForConSSVariable(rgt, lft)]
+
+    if isinstance(lft, AppliedConNSS) and isinstance(rgt, AppliedConSSS):
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    if isinstance(lft, AppliedConNSS) and isinstance(rgt, AppliedConNSS):
+        con_res = unify_con_nss(lft.con, rgt.con)
+        if isinstance(con_res, Failure):
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        if lft.arg.value != rgt.arg.value:
+            return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+        return con_res
+
+    raise NotImplementedError
+
+def unify_con_sss(
+        lft: ConcreteConSSS | VariableConSSS,
+        rgt: ConcreteConSSS | VariableConSSS,
+    ) -> UnifyResult:
+    """
+    Tries to unify the given two constuctors of kind * -> * -> *.
+    """
+    if isinstance(lft, ConcreteConSSS) and isinstance(rgt, ConcreteConSSS):
+        if lft == rgt:
+            return []
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    raise NotImplementedError
+
+def unify_con_nss(
+        lft: ConcreteConNSS | VariableConNSS,
+        rgt: ConcreteConNSS | VariableConNSS,
+    ) -> UnifyResult:
+    """
+    Tries to unify the given two constuctors of kind * -> * -> *.
+    """
+    if isinstance(lft, ConcreteConNSS) and isinstance(rgt, ConcreteConNSS):
+        if lft == rgt:
+            return []
+        return Failure(f'Cannot unify {lft.name} and {rgt.name}')
+
+    raise NotImplementedError

phasm/type5/__main__.py

@@ -0,0 +1,93 @@
+from .kindexpr import Star
+from .record import Record
+from .typeexpr import AtomicType, TypeApplication, TypeConstructor, TypeVariable
+from .unify import unify
+
+
+def main() -> None:
+    S = Star()
+
+    a_var = TypeVariable(name="a", kind=S)
+    b_var = TypeVariable(name="b", kind=S)
+    t_var = TypeVariable(name="t", kind=S >> S)
+    r_var = TypeVariable(name="r", kind=S >> S)
+    print(a_var)
+    print(b_var)
+    print(t_var)
+    print(r_var)
+    print()
+
+    u32_type = AtomicType(name="u32")
+    f64_type = AtomicType(name="f64")
+    print(u32_type)
+    print(f64_type)
+    print()
+
+    maybe_constructor = TypeConstructor(name="Maybe", kind=S >> S)
+    maybe_a_type = TypeApplication(constructor=maybe_constructor, argument=a_var)
+    maybe_u32_type = TypeApplication(constructor=maybe_constructor, argument=u32_type)
+    print(maybe_constructor)
+    print(maybe_a_type)
+    print(maybe_u32_type)
+    print()
+
+    either_constructor = TypeConstructor(name="Either", kind=S >> (S >> S))
+    either_a_constructor = TypeApplication(constructor=either_constructor, argument=a_var)
+    either_a_a_type = TypeApplication(constructor=either_a_constructor, argument=a_var)
+    either_u32_constructor = TypeApplication(constructor=either_constructor, argument=u32_type)
+    either_u32_f64_type = TypeApplication(constructor=either_u32_constructor, argument=f64_type)
+    either_u32_a_type = TypeApplication(constructor=either_u32_constructor, argument=a_var)
+    print(either_constructor)
+    print(either_a_constructor)
+    print(either_a_a_type)
+    print(either_u32_constructor)
+    print(either_u32_f64_type)
+    print(either_u32_a_type)
+    print()
+
+    t_a_type = TypeApplication(constructor=t_var, argument=a_var)
+    t_u32_type = TypeApplication(constructor=t_var, argument=u32_type)
+    print(t_a_type)
+    print(t_u32_type)
+    print()
+
+
+    shape_record = Record("Shape", [
+        ("width", u32_type),
+        ("height", either_u32_f64_type),
+    ])
+    print('shape_record', shape_record)
+    print()
+
+    values = [
+        a_var,
+        b_var,
+        u32_type,
+        f64_type,
+        t_var,
+        t_a_type,
+        r_var,
+        maybe_constructor,
+        maybe_u32_type,
+        maybe_a_type,
+        either_u32_constructor,
+        either_u32_a_type,
+        either_u32_f64_type,
+    ]
+
+    seen_exprs: set[str] = set()
+    for lft in values:
+        for rgt in values:
+            expr = f"{lft.name} ~ {rgt.name}"
+            if expr in seen_exprs:
+                continue
+
+            print(expr.ljust(40) + " => " + str(unify(lft, rgt)))
+
+            inv_expr = f"{rgt.name} ~ {lft.name}"
+            seen_exprs.add(inv_expr)
+
+        print()
+
+if __name__ == '__main__':
+    main()

phasm/type5/constraints.py

@@ -0,0 +1,54 @@
+from typing import Any, Protocol
+
+from ..build.base import BuildBase
+from .kindexpr import KindExpr, Star
+from .typeexpr import TypeExpr, TypeVariable
+
+
+
+class ExpressionProtocol(Protocol):
+    """
+    A protocol for classes that should be updated on substitution
+    """
+
+    type5: TypeExpr | None
+    """
+    The type to update
+    """
+
+class Context:
+    __slots__ = ("build", "placeholder_count", )
+
+    build: BuildBase[Any]
+    placeholder_count: int
+
+    def __init__(self, build: BuildBase[Any]) -> None:
+        self.build = build
+        self.placeholder_count = 0
+
+    def make_placeholder(self, *args: ExpressionProtocol, kind: KindExpr = Star()) -> TypeVariable:
+        self.placeholder_count += 1
+        return TypeVariable(kind, f"p_{self.placeholder_count}")
+
+class ConstraintBase:
+    __slots__ = ("ctx", "comment",)
+
+    ctx: Context
+    comment: str | None
+
+    def __init__(self, ctx: Context, comment: str | None = None) -> None:
+        self.ctx = ctx
+        self.comment = comment
+
+
+class LiteralFitsConstraint(ConstraintBase):
+    def __init__(self, ctx: Context, type: TypeExpr, val: Any, *, comment: str | None = None) -> None:
+        super().__init__(ctx, comment)
+
+        # TODO
+
+class UnifyTypesConstraint(ConstraintBase):
+    def __init__(self, ctx: Context, lft: TypeExpr, rgt: TypeExpr, *, comment: str | None = None) -> None:
+        super().__init__(ctx, comment)
+
+        # TODO

phasm/type5/fromast.py

@@ -0,0 +1,46 @@
+from typing import Any, Generator
+
+from .. import ourlang
+from .constraints import (
+    ConstraintBase,
+    Context,
+    LiteralFitsConstraint,
+    UnifyTypesConstraint,
+)
+from .typeexpr import TypeVariable
+
+ConstraintGenerator = Generator[ConstraintBase, None, None]
+
+
+def phasm_type5_generate_constraints(inp: ourlang.Module[Any]) -> list[ConstraintBase]:
+    ctx = Context(inp.build)
+
+    return [*module(ctx, inp)]
+
+def constant(ctx: Context, inp: ourlang.Constant, phft: TypeVariable) -> ConstraintGenerator:
+    if isinstance(inp, (ourlang.ConstantPrimitive, ourlang.ConstantBytes, ourlang.ConstantTuple, ourlang.ConstantStruct)):
+        yield LiteralFitsConstraint(
+            ctx, phft, inp,
+            comment='The given literal must fit the expected type'
+        )
+        return
+
+    raise NotImplementedError(constant, inp)
+
+def module_constant_def(ctx: Context, inp: ourlang.ModuleConstantDef) -> ConstraintGenerator:
+    phft = ctx.make_placeholder(inp.constant)
+
+    yield from constant(ctx, inp.constant, phft)
+    yield UnifyTypesConstraint(ctx, inp.type5, phft)
+
+def module(ctx: Context, inp: ourlang.Module[Any]) -> ConstraintGenerator:
+    for cdef in inp.constant_defs.values():
+        yield from module_constant_def(ctx, cdef)
+
+    for func in inp.functions.values():
+        if func.imported:
+            continue
+
+        # yield from function(ctx, func)
+
+        # TODO: Generalize?

phasm/type5/kindexpr.py

@@ -0,0 +1,40 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import TypeAlias
+
+
+@dataclass
+class Star:
+    def __rshift__(self, other: KindExpr) -> Arrow:
+        return Arrow(self, other)
+
+    def __str__(self) -> str:
+        return "*"
+
+@dataclass
+class Arrow:
+    """
+    Represents an arrow kind `K1 -> K2`.
+
+    To create K1 -> K2 -> K3, pass an Arrow for result_kind.
+    For now, we do not support Arrows as arguments (i.e.,
+    no higher order kinds).
+    """
+    arg_kind: Star
+    result_kind: KindExpr
+
+    def __str__(self) -> str:
+        if isinstance(self.arg_kind, Star):
+            arg_kind = "*"
+        else:
+            arg_kind = f"({str(self.arg_kind)})"
+
+        if isinstance(self.result_kind, Star):
+            result_kind = "*"
+        else:
+            result_kind = f"({str(self.result_kind)})"
+
+        return f"{arg_kind} -> {result_kind}"
+
+KindExpr: TypeAlias = Star | Arrow

phasm/type5/record.py

@@ -0,0 +1,42 @@
+from dataclasses import dataclass
+
+from .kindexpr import Star
+from .typeexpr import AtomicType, TypeApplication, TypeExpr
+
+
+@dataclass
+class Record(TypeExpr):
+    """
+    Records are a fundamental type. But we need to store some extra info.
+    """
+    fields: list[tuple[str, AtomicType | TypeApplication]]
+
+    def __init__(self, name: str, fields: list[tuple[str, AtomicType | TypeApplication]]) -> None:
+        for field_name, field_type in fields:
+            if field_type.kind == Star():
+                continue
+
+            raise TypeError(f"Record fields must be concrete types ({field_name} :: {field_type})")
+
+        super().__init__(Star(), name)
+        self.fields = fields
+
+    def __str__(self) -> str:
+        args = ", ".join(
+            f"{field_name} :: {field_type}"
+            for field_name, field_type in self.fields
+        )
+        return f"{self.name} {{{args}}} :: {self.kind}"
+
+@dataclass
+class RecordConstructor(TypeExpr):
+    """
+    TODO.
+
+    i.e.:
+    ```
+    class Foo[T, R]:
+        lft: T
+        rgt: R
+    """
+    name: str

phasm/type5/router.py

@@ -0,0 +1,8 @@
+from typing import Callable
+
+from .typeexpr import TypeExpr
+
+
+class TypeRouter[S, R]:
+    def add(self, typ: TypeExpr, mtd: Callable[[S, TypeExpr], R]) -> None:
+        raise NotImplementedError

phasm/type5/solver.py

@@ -0,0 +1,11 @@
+from typing import Any
+
+from .. import ourlang
+from .fromast import phasm_type5_generate_constraints
+
+
+def phasm_type5(inp: ourlang.Module[Any], verbose: bool = False) -> None:
+    constraint_list = phasm_type5_generate_constraints(inp)
+    assert constraint_list
+
+    raise NotImplementedError

phasm/type5/typeexpr.py

@@ -0,0 +1,52 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+
+from .kindexpr import Arrow, KindExpr, Star
+
+
+@dataclass
+class TypeExpr:
+    kind: KindExpr
+    name: str
+
+    def __str__(self) -> str:
+        return f"{self.name} :: {self.kind}"
+
+@dataclass
+class AtomicType(TypeExpr):
+    def __init__(self, name: str) -> None:
+        super().__init__(Star(), name)
+
+@dataclass
+class TypeVariable(TypeExpr):
+    """
+    A placeholder in a type expression
+    """
+
+@dataclass
+class TypeConstructor(TypeExpr):
+    name: str
+
+    def __init__(self, kind: Arrow, name: str) -> None:
+        super().__init__(kind, name)
+
+@dataclass
+class TypeApplication(TypeExpr):
+    constructor: TypeConstructor | TypeApplication | TypeVariable
+    argument: TypeExpr
+
+    def __init__(self, constructor: TypeConstructor | TypeApplication | TypeVariable, argument: TypeExpr) -> None:
+        if isinstance(constructor.kind, Star):
+            raise TypeError("A constructor cannot be a concrete type")
+
+        if constructor.kind.arg_kind != argument.kind:
+            raise TypeError("Argument does match construtor's expectations")
+
+        super().__init__(
+            constructor.kind.result_kind,
+            f"{constructor.name} {argument.name}",
+        )
+
+        self.constructor = constructor
+        self.argument = argument

phasm/type5/unify.py

@@ -0,0 +1,157 @@
+from dataclasses import dataclass
+
+from .typeexpr import (
+    AtomicType,
+    TypeApplication,
+    TypeConstructor,
+    TypeExpr,
+    TypeVariable,
+)
+
+
+@dataclass
+class Failure:
+    """
+    Both types are already different - cannot be unified.
+    """
+    msg: str
+
+@dataclass
+class Action:
+    pass
+
+class ActionList(list[Action]):
+    def __str__(self) -> str:
+        return '{' + ', '.join(map(str, self)) + '}'
+
+UnifyResult = Failure | ActionList
+
+@dataclass
+class ReplaceVariable(Action):
+    var: TypeVariable
+    typ: TypeExpr
+
+    def __str__(self) -> str:
+        return f'{self.var.name} := {self.typ.name}'
+
+def unify(lft: TypeExpr, rgt: TypeExpr) -> UnifyResult:
+    if lft == rgt:
+        return ActionList()
+
+    if lft.kind != rgt.kind:
+        return Failure("Kind mismatch")
+
+
+
+    if isinstance(lft, AtomicType) and isinstance(rgt, AtomicType):
+        return Failure("Not the same type")
+
+    if isinstance(lft, AtomicType) and isinstance(rgt, TypeVariable):
+        return ActionList([ReplaceVariable(rgt, lft)])
+
+    if isinstance(lft, AtomicType) and isinstance(rgt, TypeConstructor):
+        raise NotImplementedError  # Should have been caught by kind check above
+
+    if isinstance(lft, AtomicType) and isinstance(rgt, TypeApplication):
+        if is_concrete(rgt):
+            return Failure("Not the same type")
+
+        return Failure("Type shape mismatch")
+
+
+
+    if isinstance(lft, TypeVariable) and isinstance(rgt, AtomicType):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeVariable) and isinstance(rgt, TypeVariable):
+        return ActionList([ReplaceVariable(lft, rgt)])
+
+    if isinstance(lft, TypeVariable) and isinstance(rgt, TypeConstructor):
+        return ActionList([ReplaceVariable(lft, rgt)])
+
+    if isinstance(lft, TypeVariable) and isinstance(rgt, TypeApplication):
+        if occurs(lft, rgt):
+            return Failure("One type occurs in the other")
+
+        return ActionList([ReplaceVariable(lft, rgt)])
+
+
+
+    if isinstance(lft, TypeConstructor) and isinstance(rgt, AtomicType):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeConstructor) and isinstance(rgt, TypeVariable):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeConstructor) and isinstance(rgt, TypeConstructor):
+        return Failure("Not the same type constructor")
+
+    if isinstance(lft, TypeConstructor) and isinstance(rgt, TypeApplication):
+        return Failure("Not the same type constructor")
+
+
+
+    if isinstance(lft, TypeApplication) and isinstance(rgt, AtomicType):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeApplication) and isinstance(rgt, TypeVariable):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeApplication) and isinstance(rgt, TypeConstructor):
+        return unify(rgt, lft)
+
+    if isinstance(lft, TypeApplication) and isinstance(rgt, TypeApplication):
+        con_res = unify(lft.constructor, rgt.constructor)
+        if isinstance(con_res, Failure):
+            return con_res
+
+        arg_res = unify(lft.argument, rgt.argument)
+        if isinstance(arg_res, Failure):
+            return arg_res
+
+        return ActionList(con_res + arg_res)
+
+
+
+    return Failure('Not implemented')
+
+def occurs(lft: TypeVariable, rgt: TypeApplication) -> bool:
+    """
+    Checks whether the given variable occurs in the given application.
+    """
+    if lft == rgt.constructor:
+        return True
+
+    if lft == rgt.argument:
+        return True
+
+    if isinstance(rgt.argument, TypeApplication):
+        return occurs(lft, rgt.argument)
+
+    return False
+
+def is_concrete(lft: TypeExpr) -> bool:
+    """
+    A concrete type has no variables in it.
+
+    This is also known as a monomorphic type.
+    """
+    if isinstance(lft, AtomicType):
+        return True
+
+    if isinstance(lft, TypeVariable):
+        return False
+
+    if isinstance(lft, TypeConstructor):
+        return True
+
+    if isinstance(lft, TypeApplication):
+        return is_concrete(lft.constructor) and is_concrete(lft.argument)
+
+    raise NotImplementedError
+
+def is_polymorphic(lft: TypeExpr) -> bool:
+    """
+    A polymorphic type has one or more variables in it.
+    """
+    return not is_concrete(lft)

tests/integration/runners.py

@@ -11,6 +11,7 @@ from phasm.compiler import phasm_compile
 from phasm.optimise.removeunusedfuncs import removeunusedfuncs
 from phasm.parser import phasm_parse
 from phasm.type3.entry import phasm_type3
+from phasm.type5.solver import phasm_type5
 from phasm.wasmgenerator import Generator as WasmGenerator
 
 Imports = Optional[Dict[str, Callable[[Any], Any]]]
@@ -39,6 +40,7 @@ class RunnerBase:
         Parses the Phasm code into an AST
         """
         self.phasm_ast = phasm_parse(self.phasm_code)
+        phasm_type5(self.phasm_ast, verbose=verbose)
         phasm_type3(self.phasm_ast, verbose=verbose)
 
     def compile_ast(self) -> None:

tests/integration/test_type4/test_unify.py

@@ -0,0 +1,113 @@
+import pytest
+
+from phasm.type4 import classes
+from phasm.type4 import unify as sut
+
+
+class TestNamespace:
+    ## Kind * (part 1)
+    u32 = classes.Atomic('u32')
+    f64 = classes.Atomic('f64')
+
+    a = classes.Variable('a')
+    b = classes.Variable('b')
+
+    ## Kind * -> *
+    dynamic_array = classes.ConcreteConSS('dynamic_array')
+    maybe = classes.ConcreteConSS('maybe')
+    f = classes.VariableConSS('f')
+    t = classes.VariableConSS('t')
+
+    ## Kind * -> * -> *
+    function = classes.ConcreteConSSS('function')
+    either = classes.ConcreteConSSS('either')
+
+    ## Kind Nat -> * -> *
+    static_array = classes.ConcreteConNSS('static_array')
+
+    ## Kind * -> * (part 2)
+    function_u32 = classes.AppliedConSSS(function, u32)
+    function_f64 = classes.AppliedConSSS(function, f64)
+    either_u32 = classes.AppliedConSSS(either, u32)
+    either_f64 = classes.AppliedConSSS(either, f64)
+    static_array_4 = classes.AppliedConNSS(static_array, classes.Nat(4))
+    static_array_8 = classes.AppliedConNSS(static_array, classes.Nat(8))
+
+    ## Kind * (part 2)
+    dynamic_array_u32 = classes.AppliedConSS(dynamic_array, u32)
+    dynamic_array_f64 = classes.AppliedConSS(dynamic_array, f64)
+    maybe_u32 = classes.AppliedConSS(maybe, u32)
+    maybe_f64 = classes.AppliedConSS(maybe, f64)
+    t_u32 = classes.AppliedConSS(t, u32)
+    t_f64 = classes.AppliedConSS(t, f64)
+    f_u32 = classes.AppliedConSS(f, u32)
+    f_f64 = classes.AppliedConSS(f, f64)
+    function_f64_u32 = classes.AppliedConSS(function_f64, u32)
+    either_f64_u32 = classes.AppliedConSS(either_f64, u32)
+    static_array_4_u32 = classes.AppliedConSS(static_array_4, u32)
+    static_array_8_u32 = classes.AppliedConSS(static_array_8, u32)
+
+    TEST_LIST: list[tuple[classes.Type4, classes.Type4, sut.UnifyResult]] = [
+        # Atomic / Atomic
+        (u32, u32, []),
+        (u32, f64, sut.Failure('Cannot unify u32 and f64')),
+        # Atomic / Variable
+        (u32, a, [sut.SetTypeForVariable(a, u32)]),
+        # Atomic / AppliedConSS
+        (u32, t_f64, sut.Failure('Cannot unify u32 and t f64')),
+
+        # Variable / Atomic
+        (a, u32, [sut.SetTypeForVariable(a, u32)]),
+        # Variable / Variable
+        (a, b, [sut.ReplaceVariable(a, b)]),
+        # Variable / AppliedConSS
+        (a, t_f64, [sut.SetTypeForVariable(a, t_f64)]),
+
+        # AppliedConSS / Atomic
+        (t_f64, u32, sut.Failure('Cannot unify t f64 and u32')),
+        # AppliedConSS / Variable
+        (t_f64, a, [sut.SetTypeForVariable(a, t_f64)]),
+
+        # AppliedConSS ConcreteConSS / AppliedConSS ConcreteConSS
+        (dynamic_array_u32, dynamic_array_u32, []),
+        (dynamic_array_u32, maybe_u32, sut.Failure('Cannot unify dynamic_array u32 and maybe u32')),
+        # AppliedConSS ConcreteConSS / AppliedConSS VariableConSS
+        (dynamic_array_u32, t_u32, [sut.SetTypeForConSSVariable(t, dynamic_array)]),
+        # AppliedConSS ConcreteConSS / AppliedConSS AppliedConSSS
+        (dynamic_array_u32, function_f64_u32, sut.Failure('Cannot unify dynamic_array u32 and function f64 u32')),
+        # AppliedConSS ConcreteConSS / AppliedConSS AppliedConNSS
+        (dynamic_array_u32, static_array_4_u32, sut.Failure('Cannot unify dynamic_array u32 and static_array 4 u32')),
+
+        # AppliedConSS VariableConSS / AppliedConSS ConcreteConSS
+        (t_u32, dynamic_array_u32, [sut.SetTypeForConSSVariable(t, dynamic_array)]),
+        # AppliedConSS VariableConSS / AppliedConSS VariableConSS
+        (t_u32, f_u32, [sut.ReplaceConSSVariable(t, f)]),
+        # AppliedConSS VariableConSS / AppliedConSS AppliedConSSS
+        (t_u32, function_f64_u32, [sut.SetTypeForConSSVariable(t, function_f64)]),
+        # AppliedConSS VariableConSS / AppliedConSS AppliedConNSS
+        (t_u32, static_array_4_u32, [sut.SetTypeForConSSVariable(t, static_array_4)]),
+
+        # AppliedConSS AppliedConSSS / AppliedConSS ConcreteConSS
+        (function_f64_u32, dynamic_array_u32, sut.Failure('Cannot unify function f64 u32 and dynamic_array u32')),
+        # AppliedConSS AppliedConSSS / AppliedConSS VariableConSS
+        (function_f64_u32, t_u32, [sut.SetTypeForConSSVariable(t, function_f64)]),
+        # AppliedConSS AppliedConSSS / AppliedConSS AppliedConSSS
+        # (function_f64_u32, function_f64_u32, []),
+        (function_f64_u32, either_f64_u32, sut.Failure('Cannot unify function f64 u32 and either f64 u32')),
+        # AppliedConSS AppliedConSSS / AppliedConSS AppliedConNSS
+        (function_f64_u32, static_array_4_u32, sut.Failure('Cannot unify function f64 u32 and static_array 4 u32')),
+
+        # AppliedConSS AppliedConNSS / AppliedConSS ConcreteConSS
+        (static_array_4_u32, dynamic_array_u32, sut.Failure('Cannot unify static_array 4 u32 and dynamic_array u32')),
+        # AppliedConSS AppliedConNSS / AppliedConSS VariableConSS
+        (static_array_4_u32, t_u32, [sut.SetTypeForConSSVariable(t, static_array_4)]),
+        # AppliedConSS AppliedConNSS / AppliedConSS AppliedConSSS
+        (static_array_4_u32, function_f64_u32, sut.Failure('Cannot unify static_array 4 u32 and function f64 u32')),
+        # AppliedConSS AppliedConNSS / AppliedConSS AppliedConNSS
+        (static_array_4_u32, static_array_4_u32, []),
+        (static_array_4_u32, static_array_8_u32, sut.Failure('Cannot unify static_array 4 u32 and static_array 8 u32')),
+    ]
+
+@pytest.mark.parametrize('lft,rgt,exp_out', TestNamespace.TEST_LIST)
+def test_unify(lft: classes.Type4, rgt: classes.Type4, exp_out: sut.UnifyResult) -> None:
+    assert exp_out == sut.unify(lft, rgt)