From a55ff128afa6a1e33bdef242cf603352c43f5222 Mon Sep 17 00:00:00 2001 From: depsterr Date: Sun, 23 Jan 2022 12:00:17 +0100 Subject: [PATCH] added a TODO with some resources --- TODO | 12 ++++++++++++ test | 8 +++++++- 2 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 TODO diff --git a/TODO b/TODO new file mode 100644 index 0000000..57efb6c --- /dev/null +++ b/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 :) diff --git a/test b/test index d34a6cb..e73a3a5 100644 --- a/test +++ b/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