Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

work on variance and type variable resolution

  • Loading branch information...
commit a3e7690b7f662daf0bb2fcafd7c888553df799f6 1 parent 4147688
Ambrose Bonnaire-Sergeant authored
2  project.clj
View
@@ -1,5 +1,5 @@
(defproject typed "0.1-alpha3-SNAPSHOT"
:description "Type Checker for Clojure, as a library"
:dependencies [[org.clojure/clojure "1.4.0"]
- [analyze "0.1.6"]
+ [analyze "0.1.7-SNAPSHOT"]
[trammel "0.7.0"]])
17 src/typed/base.clj
View
@@ -1,13 +1,20 @@
(ns typed.base
(:import (clojure.lang Symbol Namespace IPersistentMap Var Keyword Namespace ISeq Seqable
- Atom IRef IObj))
+ Atom IRef IObj IPersistentList))
(:require [typed.core :refer [+T Any IParseType Nothing]]))
+(annotate-interface Seqable (a)
+
(+T typed.core/add-ns-dep [Symbol Symbol -> nil])
(+T typed.core/*add-type-ann-fn* [Symbol IParseType -> nil])
(+T typed.core/check-namespace [Symbol -> nil])
(+T clojure.core/in-ns [Symbol -> Namespace])
+(+T clojure.core/import [& (U Symbol IPersistentList) * -> nil])
+(+T clojure.core/find-ns [Symbol -> (U nil Namespace)])
+(+T clojure.core/swap! (All [x y]
+ [(Atom x) [x & y * -> x] & y * -> x]))
+;(+T clojure.core/swap! [Atom [Any & Any * -> Nothing] & Any * -> Nothing])
(+T clojure.core/resolve
(Fun [Symbol -> (U nil Var Class)]
[IPersistentMap Symbol -> (U nil Var Class)]))
@@ -33,3 +40,11 @@
(+T clojure.core/set-validator! [IRef (U nil [Nothing -> Any]) -> nil])
(+T clojure.core/partial [[Nothing & Nothing * -> Any] -> [& Nothing * -> Any]])
(+T clojure.core/with-meta [IObj (Mapof [Any Any])-> IObj])
+
+;(+T clojure.core/conj (All [x y z]
+; [nil & y ... y & z ... z * -> (IPersistentList (U y ... z))]))
+;(+T clojure.core/conj (All [x y z]
+; [(IPersistentVector x) & y ... y & z ... z * -> (IPersistentVector (U y ... z))]))
+;(+T clojure.core/conj (All [x y z] [nil & y ... y & z ... z * -> (IPersistentList (U y ... z))]))
+(+T clojure.core/conj [Seqable Any & Any * -> Seqable])
+(+T clojure.core/namespace [(U String Symbol Keyword) -> (U nil String)])
170 src/typed/core.clj
View
@@ -23,11 +23,26 @@
`(symbol (-> *ns* ns-name name) (name '~nme)))
'~type-syn))
+(def unevaled-typedcore-anns
+ "Unevaluated annotations for typed.core namespace"
+ (atom []))
+
+(declare parse-dom)
+
(def ^:dynamic
*add-type-ann-fn*
(fn [sym type-syn]
+ (when (= *ns* (find-ns 'typed.core))
+ (swap! unevaled-typedcore-anns
+ (fn [^{:- Seqable} a]
+ (conj a
+ [(if (namespace sym)
+ sym
+ (symbol "typed.core" (name sym)))
+ type-syn]))))
[sym :- type-syn]))
(+T *add-type-ann-fn* [Symbol IParseType -> nil])
+(+T unevaled-typedcore-anns Atom)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Typed require
@@ -58,7 +73,7 @@
;; Debug macros
(+T debug-mode Atom)
-(def debug-mode (atom false))
+(def debug-mode (atom true))
(+T print-warnings Atom)
(def print-warnings (atom false))
@@ -104,18 +119,20 @@
_ (binding [*add-type-ann-fn* (fn [sym type-syn]
(debug "add type:" sym :- type-syn)
(add-type-ann sym (parse type-syn)))
- *already-reloaded* (atom #{})]
+ *already-reloaded* (atom #{'typed.core})]
(reload-ns 'typed.base)
(reload-ns nsym)
- (require-typed-deps nsym))
+ (require-typed-deps nsym)
+ (doseq [[sym syntax] @unevaled-typedcore-anns]
+ (prn "add typed.core type" sym)
+ (add-type-ann sym (parse syntax))))
;; 2. Perform type checking
asts (analyze-path nsym)
_ (doseq [a asts]
(try (tc-expr a)
- (catch Exception e
- (debug a)
+ (catch Throwable e
(throw e))))]
nil))
@@ -138,10 +155,10 @@
(assert (every? TypeVariable? s))
(with-meta t {tvar-scope s}))
-(defn tvar-binding
+(defn tvar-binding
"If Type t is a binding position, return the variables binded there"
[t]
- (assert (Type? t))
+ (assert (Type? t) (class t))
(-> t meta tvar-scope))
(defn update-tvar-binding
@@ -224,17 +241,23 @@
(+T method->Fun [clojure.reflect.Method -> Fun])
(defn- method->Fun [method]
- (map->Fun
- {:arities #{(map->arity
- {:dom (->>
- (map resolve-symbol (:parameter-types method))
- (map #(if (PrimitiveClass? %)
- % ; null cannot substutitute for JVM primtiives
- (union [Nil %])))) ; Java Objects can be the null pointer
- :rng (let [typ (resolve-symbol (:return-type method))]
- (if (PrimitiveClass? typ)
- typ ; null cannot substutitute for JVM primtiives
- (union [Nil typ])))})}})) ; Java Objects can be the null pointer
+ (try
+ (map->Fun
+ {:arities #{(map->arity
+ {:dom (->>
+ (map resolve-symbol (:parameter-types method))
+ (map #(if (or (PrimitiveClass? %)
+ (subtype? Nil %))
+ % ; null cannot substutitute for JVM primtiives
+ (union [Nil %])))) ; Java Objects can be the null reference
+ :rng (let [typ (resolve-symbol (:return-type method))]
+ (if (or (PrimitiveClass? typ)
+ (subtype? Nil typ))
+ typ ; null cannot substutitute for JVM primtiives
+ (union [Nil typ])))})}}) ; Java Objects can be the null reference
+ (catch Throwable e
+ (throw (ex-info "Could not create Fun from Method" {:method method} e)))))
+
(+T var-or-class->sym [(U Var Class) -> Symbol])
(defn var-or-class->sym [var-or-class]
@@ -277,7 +300,7 @@
(every? Type? (vals m))))
(+T *type-db* (Mapof [Symbol Type]))
-(defonce ^:dynamic *type-db*
+(def ^:dynamic *type-db*
(constrained-atom {}
"Map from qualified symbols to types"
[type-db-atom-contract]))
@@ -565,6 +588,7 @@
(def-type TypeVariable [nme bnd]
"A record for bounded type variables, with an unqualified symbol as a name"
{:pre [(symbol? nme)
+ (not (primitive-symbol nme))
(not (namespace nme))
(Type? bnd)
(not (TypeVariable? bnd))]}
@@ -951,12 +975,15 @@
(parse-syntax* [this]
(parse-list-syntax this)))
+(defn- split-no-check [arity-syntax]
+ (let [[dom [_ rng & opts]] (split-with #(not= '-> %) arity-syntax)]
+ [dom rng (apply hash-map opts)]))
+
(defn- split-arity-syntax
"Splits arity syntax into [dom rng opts-map]"
[arity-syntax]
(assert (some #(= '-> %) arity-syntax) (str "Arity " arity-syntax " missing return type"))
- (let [[dom [_ rng & opts]] (split-with #(not= '-> %) arity-syntax)]
- [dom rng (apply hash-map opts)]))
+ (split-no-check arity-syntax))
(defn- parse-filter [syn]
(assert (vector? syn))
@@ -970,18 +997,32 @@
{:var nme-sym
:type type}))))
+(defn- parse-dom
+ "Given syntax to the left of an arrow, returns a map with keys
+ :dom, :rest-type"
+ [dom]
+ (let [[fixed-dom [_ & rest-args]]
+ (split-with #(not= '& %) dom)
+
+ uniform-rest-syntax (when (seq rest-args)
+ (if (= '* (second rest-args))
+ (first rest-args)
+ (assert false (str "Invalid rest args syntax " dom))))
+
+ fixed-dom-types (doall (map parse-syntax fixed-dom))
+ uniform-rest-type (when rest-args
+ (parse-syntax uniform-rest-syntax))]
+ {:dom fixed-dom-types
+ :rest-type uniform-rest-type}))
+
(extend-protocol IParseType
IPersistentVector
(parse-syntax* [this]
(let [[dom rng opts-map] (split-arity-syntax this)
- [fixed-dom [_ & rest-args]]
- (split-with #(not= '& %) dom)
-
- uniform-rest-syntax (when (seq rest-args)
- (if (= '* (second rest-args))
- (first rest-args)
- (assert false (str "Invalid rest args syntax " this))))
+ {fixed-dom-types :dom
+ rest-type :rest-type}
+ (parse-dom dom)
extras (into {}
(for [[nme syn] opts-map]
@@ -992,16 +1033,13 @@
:else (throw (Exception. (str "Unsupported option " nme))))))
- fixed-dom-types (doall (map parse-syntax fixed-dom))
- rng-type (parse-syntax rng)
- uniform-rest-type (when rest-args
- (parse-syntax uniform-rest-syntax))]
+ rng-type (parse-syntax rng)]
(map->arity
(merge
{:dom fixed-dom-types
:rng rng-type}
- (when uniform-rest-type
- {:rest-type uniform-rest-type})))))
+ (when rest-type
+ {:rest-type rest-type})))))
nil
(parse-syntax* [_]
@@ -1924,7 +1962,7 @@
(let [[sub-dom sup-dom]
(align-doms a-sub a-sup)
- dom-constraint-sets (map constraint-gen sup-dom sub-dom)
+ dom-constraint-sets (doall (map constraint-gen sup-dom sub-dom))
rng-constraint-set (constraint-gen (:rng a-sub) (:rng a-sup))]
(apply intersect-constraint-sets rng-constraint-set dom-constraint-sets)))
@@ -1996,7 +2034,7 @@
(let [[sub-dom sup-dom]
(align-doms a-sub a-sup)
- dom-constraint-sets (map match-constraint sup-dom sub-dom)
+ dom-constraint-sets (doall (map match-constraint sup-dom sub-dom))
rng-constraint-set (match-constraint (:rng a-sub) (:rng a-sup))]
(apply intersect-constraint-sets rng-constraint-set dom-constraint-sets)))
@@ -2067,6 +2105,10 @@
ClassType
(collect-variances [this xs m] m)
+ Vector
+ (collect-variances [this xs m]
+ (collect-variances (:type this) xs m))
+
TypeVariable
(collect-variances [this xs m]
(let [bnd-variances (collect-variances (:bnd this) xs m)]
@@ -2079,21 +2121,22 @@
Union
(collect-variances [this xs m]
(apply merge-with update-variance
- (map #(collect-variances % xs m) (:types this))))
+ (doall (map #(collect-variances % xs m) (:types this)))))
Fun
(collect-variances [this xs m]
(apply
merge-with update-variance
- (map #(collect-variances % xs m) (:arities this))))
+ (doall (map #(collect-variances % xs m) (:arities this)))))
arity
(collect-variances [this xs m]
(let [dom-variances (with-flipped-variance
- (map #(collect-variances % xs m)
+ (doall
+ (map #(collect-variances % xs m)
(concat (:dom this)
(when (:rest-type this)
- [(:rest-type this)]))))
+ [(:rest-type this)])))))
rng-variances (collect-variances (:rng this) xs m)]
(apply merge-with update-variance
(concat dom-variances [rng-variances])))))
@@ -2117,6 +2160,38 @@
(max-type [this] (:upper this))
(min-type [this] (:lower this)))
+(defn gen-substitution
+ "Given a type and a satisfiable constraint set, return the substitution map"
+ [t xs cs]
+ {:post [(map? %)
+ (every? TypeVariable? (keys %))
+ (every? Type? (vals %))]}
+ (assert (Type? t))
+ (assert (ConstraintSet? cs))
+ (assert (set? xs))
+ (assert (every? TypeVariable? xs))
+ (let [cs (:cs cs)
+ variance (with-covariance
+ (calculate-variances t xs))]
+ (into {}
+ (for [x xs]
+ [x
+ (cond
+ (= covariant (variance x))
+ (min-type (cs x))
+
+ (= contravariant (variance x))
+ (max-type (cs x))
+
+ (= invariant (variance x))
+ (min-type (cs x))
+
+ ;;TODO rigid?
+
+ :else
+ (throw (Exception. "No variance")))]))))
+
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Type Inference
@@ -2304,12 +2379,18 @@
(assoc expr
type-key mtched-arity)))
+(defmacro parse-params [dom-syn]
+ `(parse-dom '~dom-syn))
+
+(def annotate-param-syntax :-)
+(def annotate-dom-syntax :-params)
+
(defn synthesize-fn-method
[{:keys [required-params rest-param] :as expr}]
(letfn [(meta-type-annot [expr]
- (assert (-> expr :sym meta (find '+T))
+ (assert (-> expr :sym meta (find annotate-param-syntax))
(str "No type for parameter " (-> expr :sym)))
- (-> expr :sym meta (get '+T) parse))]
+ (-> expr :sym meta (get annotate-param-syntax) parse))]
(let [dom-syms (map :sym required-params)
rest-sym (:sym rest-param)
@@ -2514,9 +2595,8 @@
(defmulti empty-types class)
-(defmethod empty-types IPersistentMap
- [m]
- (->Map [Nothing Nothing]))
+(defmethod empty-types IPersistentMap [m] (->Map [Nothing Nothing]))
+(defmethod empty-types IPersistentVector [m] (->Vector Nothing))
(defmethod tc-expr :empty-expr
[{:keys [coll] :as expr} & opts]
205 test/typed/test/core.clj
View
@@ -208,97 +208,133 @@
(parse '~tsyn)))
(deftest variance-type-variables
- ; with covariance
- (is (let [x (-tv 'x)
- variance (with-covariance
- (calculate-variances x #{x}))]
- (= {x covariant}
- variance)))
- ; with contravariance
- (is (let [x (-tv 'x)
- variance (with-contravariance
- (calculate-variances x #{x}))]
- (= {x contravariant}
- variance)))
- ; in a scope
- (is (let [x (-tv 'x)
- t (with-frees [x]
- (All [y] x))
- variance (with-covariance
- (calculate-variances t #{x}))]
- (= {x covariant}
- variance)))
- ; in a scope
- (is (let [x (-tv 'x)
- t (with-frees [x]
- (All [y] x))
- variance (with-covariance
- (calculate-variances t #{x}))]
- (= {x covariant}
- variance))))
+ (testing "with covariance"
+ (is (let [x (-tv 'x)
+ variance (with-covariance
+ (calculate-variances x #{x}))]
+ (= {x covariant}
+ variance))))
+ (testing "with contravariance"
+ (is (let [x (-tv 'x)
+ variance (with-contravariance
+ (calculate-variances x #{x}))]
+ (= {x contravariant}
+ variance))))
+ (testing "in a scope"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ (All [y] x))
+ variance (with-covariance
+ (calculate-variances t #{x}))]
+ (= {x covariant}
+ variance))))
+ (testing "shadowed (x does not occur)"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ (All [x] x))
+ variance (with-covariance
+ (calculate-variances t #{x}))]
+ (= {}
+ variance)))))
(deftest variance-function-fixed-domain
- ;function domain, with covariance
- (is (let [x (-tv 'x)
- t (with-frees [x]
- (All [y] [x -> y]))
- variance (with-covariance
- (calculate-variances t #{x}))]
- (= {x contravariant}
- variance)))
- ;function domain, with contravariance
- (is (let [x (-tv 'x)
- t (with-frees [x]
- (All [y] [x -> y]))
- variance (with-contravariance
- (calculate-variances t #{x}))]
- (= {x covariance}
- variance))))
+ (testing "function domain, with covariance"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ (All [y] [x -> y]))
+ variance (with-covariance
+ (calculate-variances t #{x}))]
+ (= {x contravariant}
+ variance))))
+ (testing "function domain, with contravariance"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ (All [y] [x -> y]))
+ variance (with-contravariance
+ (calculate-variances t #{x}))]
+ (= {x covariant}
+ variance)))))
(deftest variance-function-rest-type
- ;function rest type, with covariance
- (is (let [x (-tv 'x)
- t (with-frees [x]
- (All [y] [& x * -> y]))
- variance (with-covariance
- (calculate-variances t #{x}))]
- (= {x contravariant}
- variance)))
- ;function rest type, with contravariance
+ (testing "function rest type, with covariance"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ (All [y] [& x * -> y]))
+ variance (with-covariance
+ (calculate-variances t #{x}))]
+ (= {x contravariant}
+ variance))))
+ (testing "function rest type, with contravariance"
(is (let [x (-tv 'x)
t (with-frees [x]
(All [y] [& x * -> y]))
variance (with-contravariance
(calculate-variances t #{x}))]
- (= {x covariance}
- variance))))
+ (= {x covariant}
+ variance)))))
(deftest variance-function-range
- ;function range, with covariance
- (is (let [x (-tv 'x)
- t (with-frees [x]
- (All [y] [y -> x]))
- variance (with-covariance
- (calculate-variances t #{x}))]
- (= {x covariant}
- variance)))
- ;function range, with contravariance
- (is (let [x (-tv 'x)
- t (with-frees [x]
- (All [y] [y -> x]))
- variance (with-contravariance
- (calculate-variances t #{x}))]
- (= {x contravariance}
- variance))))
+ (testing "function range, with covariance"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ (All [y] [y -> x]))
+ variance (with-covariance
+ (calculate-variances t #{x}))]
+ (= {x covariant}
+ variance))))
+ (testing "function range, with contravariance"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ (All [y] [y -> x]))
+ variance (with-contravariance
+ (calculate-variances t #{x}))]
+ (= {x contravariant}
+ variance)))))
(deftest invariant-tests
- (is (let [x (-tv 'x)
- t (with-frees [x]
- [x -> x])
- variance (with-covariance
- (calculate-variances t #{x}))]
- (= {x invariant}
- variance))))
+ (testing "variable on both sides of arrow"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ [x -> x])
+ variance (with-covariance
+ (calculate-variances t #{x}))]
+ (= {x invariant}
+ variance)))))
+
+(deftest variance-calc-complex-nesting
+ (testing "variance in nested functions"
+ (is (let [x (-tv 'x)
+ y (-tv 'y)
+ z (-tv 'z)
+ t (with-frees [x y z]
+ [x y x & [z -> x] * -> [x -> y]])
+ variance (with-covariance
+ (calculate-variances t #{x y z}))]
+ (= {x contravariant
+ y invariant
+ z covariant}
+ variance)))))
+
+(deftest variance-calc-bnds
+ (testing "variable in bound"
+ (testing "covariant"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ (All [(y <! (Vectorof x))]
+ y))
+ variance (with-covariance
+ (calculate-variances t #{x}))]
+ (= {x covariant}
+ variance)))))
+ (testing "contravariant"
+ (is (let [x (-tv 'x)
+ t (with-frees [x]
+ (All [(y <! (Vectorof x))]
+ y))
+ variance (with-contravariance
+ (calculate-variances t #{x}))]
+ (= {x contravariant}
+ variance)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Equality
@@ -382,7 +418,6 @@
(is (sub? char Object))
(is (sub? boolean Object))
(is (not (sub? nil Object)))
- (is (not (sub? nil Object)))
(is (sub? Object Object)))
(deftest subtype-fun
@@ -434,8 +469,6 @@
(is (sub? (U)
(U)))
(is (sub? (U)
- (U)))
- (is (sub? (U)
(U Object nil)))
(is (not (sub? (U Object nil)
(U))))
@@ -709,9 +742,15 @@
(fn [] 1)
[-> 1]))
(is (subfrm
- (fn [^{+T Long} b]
+ (fn [^{:- Long} b]
b)
- [Long -> Long])))
+ [Long -> Long]))
+ (is (let [f
+ ^{:-params [Seqable]}
+ #(conj % 1)]
+ (subfrm
+ f
+ [Seqable -> Seqable]))))
(deftest tc-expr-fn-rest-type
(is (subfrm
Please sign in to comment.
Something went wrong with that request. Please try again.