From 0a056ebef269f52ee289668a1e235030857638dc Mon Sep 17 00:00:00 2001 From: Nathan Braswell Date: Sun, 24 Jan 2021 02:53:55 -0500 Subject: [PATCH] Limited monomorphic-only Damas-Hindley-Milner implemented in types --- k_prime.krak | 11 ++++-- prelude.kp | 17 +++++++++ types.kp | 95 ++++++++++++++++++++++++++++++++------------------- types_test.kp | 2 +- 4 files changed, 86 insertions(+), 39 deletions(-) diff --git a/k_prime.krak b/k_prime.krak index 1d6f1a1..74f5078 100644 --- a/k_prime.krak +++ b/k_prime.krak @@ -835,6 +835,13 @@ fun main(argc: int, argv: **char): int { return make_pair(null(), KPResult::Ok(kpBool(params[0].is_symbol()))) })); + env->set(str("int?"), make_builtin_combiner(str("symbol?"), 1, false, fun(params: vec, dynamic_env: *KPEnv): pair<*KPEnv, KPResult> { + if params.size != 1 { + return make_pair(null(), KPResult::Err(kpString(str("Need 1 param to int?")))) + } + return make_pair(null(), 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, dynamic_env: *KPEnv): pair<*KPEnv, KPResult> { if params.size != 1 { return make_pair(null(), 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(), KPResult::Err(kpString(str("Need 1 param to len")))) } if !params[0].is_array() && !params[0].is_string() { - return make_pair(null(), KPResult::Err(kpString(str("Called len with not an array/string ") + pr_str(params[0], true)))) + return make_pair(null(), 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(), 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(), KPResult::Err(kpString(str("Need 2 params to idx")))) } if !params[0].is_array() && !params[0].is_string() { return make_pair(null(), 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(), KPResult::Err(kpString(str("Param 2 to idx is not int")))); } + if !params[1].is_int() { return make_pair(null(), 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 { diff --git a/prelude.kp b/prelude.kp index 793dd39..2d37a34 100644 --- a/prelude.kp +++ b/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 diff --git a/types.kp b/types.kp index 074c41f..3962847 100644 --- a/types.kp +++ b/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]) - get_exp (lambda (et) (idx et 0)) - get_typ (lambda (et) (idx et 1)) - get_ret_typ (lambda (f_typ) (idx f_typ 1)) - get_params_typs (lambda (f_typ) (idx f_typ 0)) - types_match (lambda (t1 t2) (= t1 t2)) + contains (let (contains-helper (rec-lambda recurse (s x i) (cond (= i (len s)) false + (= x (idx s i)) true + true (recurse s x (+ i 1))))) + (lambda (s x) (contains-helper s x 0))) - 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))) - symbol_type_com (lambda (sym) (lambda (env) (with_type sym (lookup env sym)))) + execute_type_com (lambda (tc e idn) (tc e idn)) + + 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 (get_exp f_et) - f_t (get_typ f_et) - p_et (map (lambda (x) (execute_type_com x env)) (slice innards 1 -1)) - p_e (map get_exp p_et) - p_t (map get_typ p_et) - ) (if (parameter_types_match f_t p_t) - (with_type (cons f_e p_e) (get_ret_typ f_t)) - (error (str "Function type (" f_t ") does not match parameter types (" p_t ")")) - ) - ) + (f_e f_t S_0 idn) (execute_type_com (idx innards 0) env idn) + across_params (rec-lambda recurse (env S idn params i out_e out_t) + (if (= i (len params)) [out_e out_t S idn] + (let ( + (p_e p_t S_i idn) (execute_type_com (idx params i) env idn) + ) (recurse (applySE S_i env) (applySS S_i S) idn params (+ 1 i) (concat out_e [p_e]) (concat out_t [p_t]))))) + (p_es p_ts S_ps idn) (across_params (applySE S_0 env) [] idn (slice innards 1 -1) 0 [] []) + (r_t idn) [idn (+ 1 idn)] + 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) - b_et (execute_type_com b extended_env) - b_t (get_typ b_et) - b_e (get_exp b_et) + (p_t idn) (if (= nil t) [idn (+ 1 idn)] + [t idn]) + extended_env (cons [p p_t] env) + (b_e b_t S idn) (execute_type_com b extended_env idn) f_e [lambda [p] b_e] - f_t [[t] b_t] - ) (with_type f_e f_t)) + f_t [[ (applyST S p_t) ] b_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) diff --git a/types_test.kp b/types_test.kp index 8ab4818..15a4e85 100644 --- a/types_test.kp +++ b/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)