added a TODO with some resources

TODO

@@ -0,0 +1,12 @@
+1) Write a Hindley Milner type checker for that injective datatype recursor language
+
+https://wikimedia.org/api/rest_v1/media/math/render/svg/431b94815103ac9dc77d0e92739456c3c2c90803
+https://github.com/sdiehl/write-you-a-haskell/blob/master/chapter7/poly_constraints/src/Infer.hs
+https://github.com/sdiehl/write-you-a-haskell/blob/master/chapter7/poly/src/Infer.hs
+
+2) Extend it to allow for referencing declerations "further down" in file, but make sure it
+terminates by forbidding corecursion (simply done by building a reference graph and then looking at it)
+
+3) Add Kind env and use it to have "type of types"
+
+4) Then make the SECD machine good enough to execute it :)

test

@@ -1,17 +1,23 @@
+-- currently all parameterised types are commented out until kinds are being implemented
+
 -- no pattern matching, instead a recursor is given based on your inductive definition
 -- for example: the following
 
+{-
 type List A
   | nil : List A
   |	cons  : A → List A → List A
+-}
 
 -- will bring the following into scope
 -- rec[List] : B → (A → B → B) → List A → B
 
 -- map could then be written as
-
+ 
+{-
 map : (A → B) → List A → List B
  := rec[List] nil (λx xs. cons (f x) xs)
+-}
 
 -- one could then define the naturals as follows