ideas

phasm/type4/classes.py

@@ -0,0 +1,132 @@
+from __future__ import annotations
+
+from typing import TypeAlias
+
+from dataclasses import dataclass
+
+## 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,201 @@
+from dataclasses import dataclass
+
+from .classes import (
+    AppliedConNSS,
+    AppliedConSS,
+    AppliedConSSS,
+    Atomic,
+    ConcreteConNSS,
+    ConcreteConSS,
+    ConcreteConSSS,
+    Variable,
+    VariableConNSS,
+    VariableConSS,
+    VariableConSSS,
+    Type4
+)
+
+@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

tests/integration/test_type4/test_unify.py

@@ -0,0 +1,115 @@
+from typing import Sequence
+
+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)