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/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')
 

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: