diff --git a/TODO.md b/TODO.md index 0757ab3..88c672d 100644 --- a/TODO.md +++ b/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) diff --git a/phasm/type3/constraintsgenerator.py b/phasm/type3/constraintsgenerator.py index a666885..7270973 100644 --- a/phasm/type3/constraintsgenerator.py +++ b/phasm/type3/constraintsgenerator.py @@ -279,6 +279,47 @@ def statement_return(ctx: Context, fun: ourlang.Function, inp: ourlang.Statement yield from expression(ctx, inp.value, phft) + # callme :: (a -> b) -> a -> b :: * + # def callme(fun: (a -> b), arg: a) -> b: + # return fun(arg) + + # todouble :: u32 -> f32 :: * + # def todouble(in: u32) -> f32: + # .... + + # def main(): + # print(callme(todouble, 15)) + + # dynamic_array :: * -> * + # static_array :: Int -> * -> * + # + # class Foldable f + # + # instance Foldable (static_array n) + # + # def foo(r: u32[4], l: u32[...]) -> ... + # + # + + # def foo(in: a[4]) -> a[4]: + + + # def min(lft: a, rgt: a) -> a: + # if lft < rgt: + # return lft + # return rgt + # + # min :: NatNum a => a -> a -> a + # + # main :: IO + # main = do + # show $ min 3 4 + # show $ min 3.1 3.2 + + # a ~ b => b := a + # a ~ c => c := a + # a ~ a => ignore + yield SameTypeConstraint(ctx, fun.returns_type3, phft, comment=f'The type of the value returned from function {fun.name} should match its return type') diff --git a/phasm/type3/types.py b/phasm/type3/types.py index 9406c1b..75fb068 100644 --- a/phasm/type3/types.py +++ b/phasm/type3/types.py @@ -243,6 +243,26 @@ class TypeConstructor_TypeStar(TypeConstructor_Base[Tuple[Type3, ...]]): class TypeApplication_TypeStar(TypeApplication_Base[TypeConstructor_TypeStar, Tuple[Type3, ...]]): pass +# head :: [a] -> a + +# (+) :: NatNum a => a -> a -> a +# instancen NatNum f32 +# (+) :: wasm_f32_add + +# inc1 :: NatNum a => a -> a +# inc1 = (+) 1 + +# data Type3 +# | Type3KindS String None +# | Type3KindS_S String Type3 +# | Type3KindS_S_S String Type3 Type3 + +# data TypeVariable3 +# | TypeVariable3KindS String None +# | TypeVariable3KindS_S String Type3 +# | TypeVariable3KindS_S_S String Type3 Type3 + + class TypeConstructor_DynamicArray(TypeConstructor_Type): def make_name(self, key: Tuple[Type3]) -> str: if 'u8' == key[0].name: