Limited monomorphic-only Damas-Hindley-Milner implemented in types

k_prime.krak

@@ -835,6 +835,13 @@ fun main(argc: int, argv: **char): int {
         return make_pair(null<KPEnv>(), KPResult::Ok(kpBool(params[0].is_symbol())))
     }));
 
+    env->set(str("int?"), make_builtin_combiner(str("symbol?"), 1, false, fun(params: vec<KPValue>, dynamic_env: *KPEnv): pair<*KPEnv, KPResult> {
+        if params.size != 1 {
+            return make_pair(null<KPEnv>(), KPResult::Err(kpString(str("Need 1 param to int?"))))
+        }
+        return make_pair(null<KPEnv>(), KPResult::Ok(kpBool(params[0].is_int())))
+    }));
+
     env->set(str("str-to-symbol"), make_builtin_combiner(str("str-to-symbol"), 1, false, fun(params: vec<KPValue>, dynamic_env: *KPEnv): pair<*KPEnv, KPResult> {
         if params.size != 1 {
             return make_pair(null<KPEnv>(), KPResult::Err(kpString(str("Need 1 param to str-to-symbol"))))
@@ -869,7 +876,7 @@ fun main(argc: int, argv: **char): int {
             return make_pair(null<KPEnv>(), KPResult::Err(kpString(str("Need 1 param to len"))))
         }
         if !params[0].is_array() && !params[0].is_string() {
-            return make_pair(null<KPEnv>(), KPResult::Err(kpString(str("Called len with not an array/string ") + pr_str(params[0], true))))
+            return make_pair(null<KPEnv>(), KPResult::Err(kpString(str("Called len with not an array/string ") + pr_str(params[0], true) + "\nenv was\n" + dynamic_env->to_string())))
         }
         if params[0].is_array() {
             return make_pair(null<KPEnv>(), KPResult::Ok(kpInt(params[0].get_array_rc().get().size)))
@@ -882,7 +889,7 @@ fun main(argc: int, argv: **char): int {
             return make_pair(null<KPEnv>(), KPResult::Err(kpString(str("Need 2 params to idx"))))
         }
         if !params[0].is_array() && !params[0].is_string() { return make_pair(null<KPEnv>(), KPResult::Err(kpString(str("Param 1 to idx is not string or array") + pr_str(params[0], true)))); }
-        if !params[1].is_int() { return make_pair(null<KPEnv>(), KPResult::Err(kpString(str("Param 2 to idx is not int")))); }
+        if !params[1].is_int() { return make_pair(null<KPEnv>(), KPResult::Err(kpString(str("Param 2 to idx is not int ") + pr_str(params[1], true)))); }
 
         var index = params[1].get_int()
         if index < 0 {

prelude.kp

@@ -98,6 +98,22 @@
                                                 n
                                                 (recurse f l (concat n (f (idx l i))) (+ i 1)))))
                  (helper f l (array) 0)))
+        flat_map_i (lambda (f l)
+            (let (helper (rec-lambda recurse (f l n i)
+                                            (if (= i (len l))
+                                                n
+                                                (recurse f l (concat n (f i (idx l i))) (+ i 1)))))
+                 (helper f l (array) 0)))
+        ; with all this, we make a destrucutring-capable let
+        let (let (
+            destructure_helper (rec-lambda recurse (vs i r)
+                (cond (= (len vs) i)      r
+                      (array? (idx vs i)) (let (bad_sym (str-to-symbol (str (idx vs i)))
+                                                new_vs (flat_map_i (lambda (i x) (array x (array idx bad_sym i))) (idx vs i))
+                                                )
+                                                (recurse (concat new_vs (slice vs (+ i 2) -1)) 0 (concat r (array bad_sym (idx vs (+ i 1))))))
+                      true                (recurse vs (+ i 2) (concat r (slice vs i (+ i 2))))
+            ))) (vau de (vs b) (vapply let (array (destructure_helper vs 0 (array)) b) de)))
 
         is_pair? (lambda (x) (and (array? x) (> (len x) 0)))
 
@@ -173,6 +189,7 @@
                                 map
                                 map_i
                                 flat_map
+                                flat_map_i
                                 lapply
                                 vapply
                                 Y

types.kp

@@ -7,54 +7,72 @@
                                                                     (recurse dict key (+ i 1))))))
                    (lambda (dict key) (lookup-helper dict key 0)))
 
-    with_type   (lambda (exp typ) [exp typ])
+    contains (let (contains-helper (rec-lambda recurse (s x i) (cond (= i (len s))   false
-    get_exp     (lambda (et)      (idx et 0))
+                                                                     (= x (idx s i)) true
-    get_typ     (lambda (et)      (idx et 1))
+                                                                     true            (recurse s x (+ i 1)))))
-    get_ret_typ (lambda (f_typ)   (idx f_typ 1))
+                   (lambda (s x) (contains-helper s x 0)))
-    get_params_typs (lambda (f_typ)   (idx f_typ 0))
-    types_match (lambda (t1 t2)   (= t1 t2))
 
-    execute_type_com (lambda (tc e) (tc e))
+    applyST (rec-lambda recurse (S t)
+                (cond
+                    (int? t)    (or  (lookup S t) t)
+                    (array? t)  (map (lambda (x) (recurse S x)) t)
+                    true t
+    ))
+    applySE (lambda (S env) (map (lambda (x) [(idx x 0) (applyST S (idx x 1))]) env))
+    applySS (lambda (S_0 S_1) (let (r (concat S_0 (applySE S_0 S_1)) _ (println "applySS of " S_0 " and " S_1 " is " r)) r))
+    fvT (rec-lambda recurse (t) (cond (symbol? t) [t]
+                                      (array? t)  (flat_map recurse t)
+                                      true        []
+    ))
+    fvE (lambda (env) (flat_map (lambda (x) (fvT (idx x 1))) env))
+    varBind (lambda (a b) (cond
+                            (= a b) []
+                            (contains (fvT b) a) (error "Contains check failed for " a " and " b)
+                            true [ [a b] ]))
+    mgu (rec-lambda mgu (a b) (let (r (cond
+                        (and (array? a) (array? b) (= (len a) (len b))) ((rec-lambda recurse (S i) (if (= i (len a)) S
+                                                                                                                     (recurse (applySS (mgu (idx a i) (idx b i)) S) (+ 1 i)))) [] 0)
+                        (int? a) (varBind a b)
+                        (int? b) (varBind b a)
+                        (= a b)  []
+                        true     (error (str "Cannot unify " a " " b))
+    ) _ (println "mgu of " a " and " b " is " r)) r))
 
-    simple_type_com (lambda (exp typ) (lambda (env) (with_type exp typ)))
+    execute_type_com (lambda (tc e idn) (tc e idn))
-    symbol_type_com (lambda (sym)     (lambda (env) (with_type sym (lookup env sym))))
+
+    simple_type_com (lambda (exp typ) (lambda (env idn) [exp typ [] idn]))
+    symbol_type_com (lambda (sym)     (lambda (env idn) [sym (lookup env sym) [] idn]))
 
-    parameter_types_match (let (pmth (rec-lambda recurse (l1 l2 i) (cond (= i (len l1))                      true
-                                                                         (types_match (idx l1 i) (idx l2 i)) (recurse l1 l2 (+ i 1))
-                                                                         true                                false)))
-                               (lambda (f_t pt) (let (fp_t (get_params_typs f_t))
-                                                    (if (= (len fp_t) (len pt))
-                                                        (pmth fp_t pt 0)
-                                                        false))))
     call_type_com (lambda (innards)
-        (lambda (env)
+        (lambda (env idn)
             (if (= 0 (len innards)) (error "stlc_error: Can't have a 0-length call")
                 (let (
-                    f_et (execute_type_com (idx innards 0) env)
+                    (f_e f_t S_0 idn) (execute_type_com (idx innards 0) env idn)
-                    f_e (get_exp f_et)
+                    across_params (rec-lambda recurse (env S idn params i out_e out_t)
-                    f_t (get_typ f_et)
+                                    (if (= i (len params)) [out_e out_t S idn]
-                    p_et (map (lambda (x) (execute_type_com x env)) (slice innards 1 -1))
+                                                           (let (
-                    p_e  (map get_exp p_et)
+                                                                (p_e p_t S_i idn) (execute_type_com (idx params i) env idn)
-                    p_t  (map get_typ p_et)
+                                                                ) (recurse (applySE S_i env) (applySS S_i S) idn params (+ 1 i) (concat out_e [p_e]) (concat out_t [p_t])))))
-                ) (if (parameter_types_match f_t p_t)
+                    (p_es p_ts S_ps idn) (across_params (applySE S_0 env) [] idn (slice innards 1 -1) 0 [] [])
-                      (with_type (cons f_e p_e) (get_ret_typ f_t))
+                    (r_t idn) [idn (+ 1 idn)]
-                      (error (str "Function type (" f_t ") does not match parameter types (" p_t ")"))
+                    S_f (mgu (applyST S_ps f_t) [p_ts r_t])
-                  )
+                    _ (println "mgu of " (applyST S_ps f_t) " and " [p_ts r_t] " produces substitution " S_f)
-                )
+                    _ (println "For this call: " (cons f_e p_es) " the return type " r_t " transformed by " S_f " is " (applyST S_f r_t))
+                ) [(cons f_e p_es) (applyST S_f r_t) (applySS S_f (applySS S_ps S_0)) idn])
             )
         )
     )
 
     lambda_type_com (lambda (p t b)
-        (lambda (env)
+        (lambda (env idn)
             (let (
-                extended_env (cons [p t] env)
+                (p_t idn) (if (= nil t) [idn (+ 1 idn)]
-                b_et (execute_type_com b extended_env)
+                                        [t   idn])
-                b_t (get_typ b_et)
+                extended_env (cons [p p_t] env)
-                b_e (get_exp b_et)
+                (b_e b_t S idn) (execute_type_com b extended_env idn)
                 f_e [lambda [p] b_e]
-                f_t [[t] b_t]
+                f_t [[ (applyST S p_t) ] b_t]
-            ) (with_type f_e f_t))
+            ) [f_e f_t S idn])
         )
     )
 
@@ -68,6 +86,10 @@
     current_env (vau de () de)
     syms (map (lambda (x) (idx x 0)) base_env)
     builtin_real_env (eval (concat (vapply provide syms root_env) [[current_env]]) empty_env)
+    top-level-erase-and-check (lambda (e) (let (
+                                            (e t S idn) (execute_type_com e base_env 0)
+                                            _ (println "Type of program is " t " with sub " S)
+                                          ) e))
 
     stlc (concat basic_rules [
 
@@ -80,12 +102,13 @@
                                                   )
                                                  ) ]
         [ 'expr [ "\\\\" 'WS * 'bool_nil_symbol 'WS * ":" 'WS * 'bool_nil_symbol 'WS * "." 'WS * 'expr ] (lambda (_ _ p _ _ _ t _ _ _ b) (lambda_type_com p t b)) ]
+        [ 'expr [ "\\\\" 'WS * 'bool_nil_symbol 'WS * "." 'WS * 'expr ] (lambda (_ _ p _ _ _ b) (lambda_type_com p nil b)) ]
 
         [ 'call_innards [ 'WS * ]                 (lambda (_)   []) ]
         [ 'call_innards [ 'expr [ 'WS 'expr ] * ] (lambda (f r) (cons f (map (lambda (x) (idx x 1)) r))) ]
         [ 'expr [ "\\(" 'call_innards "\\)" ] (lambda (_ innards _) (call_type_com innards)) ]
 
-        [ 'stlc_start_symbol [ 'WS * 'expr 'WS * ] (lambda (_ e _) [eval (get_exp (execute_type_com e base_env)) builtin_real_env]) ]
+        [ 'stlc_start_symbol [ 'WS * 'expr 'WS * ] (lambda (_ e _) [eval (top-level-erase-and-check e) builtin_real_env]) ]
 
    ]))
    (provide stlc)

types_test.kp

@@ -1,2 +1,2 @@
 #lang (with_import "./types.kp" stlc) stlc_start_symbol
-(\ x : int . (+ x 1) 2)
+(\ x  . (+ x 1337) 12)