Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Start type rep with datatypes/protocols

  • Loading branch information...
commit 0a23a69d417408ee47822a3758e96814653845df 1 parent fa7dda7
@frenchy64 authored
Showing with 195 additions and 47 deletions.
  1. +179 −47 src/typed/core.clj
  2. +16 −0 test/typed/test/example.clj
View
226 src/typed/core.clj
@@ -29,35 +29,54 @@
;; Type Rep
-(deftype FunctionType [arities])
-(deftype ArityType [dom rng rest])
-(deftype PolyConstructorType [tvars scope])
+(deftype FunctionType [dom rng has-uniform-rest uniform-rest]
+ Object
+ (toString [this]
+ (str (vec (doall (concat dom
+ (when has-uniform-rest
+ ['& uniform-rest '*])
+ ['-> rng]))))))
+(deftype PolyConstructorType [tvars scope]
+ Object
+ (toString [this]
+ (str (list 'All (mapv #(vector (.nme %) :< (.bound %) :variance (.variance %)) tvars)
+ scope))))
(deftype PolyInstanceType [constructor insts])
-(deftype TV [nme bound variance])
-(deftype UnionType [types])
-(deftype CaseType [types])
-(deftype IntersectionType [types])
+(deftype TV [nme bound variance]
+ Object
+ (toString [this]
+ (str nme)))
+(deftype UnionType [types]
+ Object
+ (toString [this]
+ (str (apply list 'U types))))
+(deftype IntersectionType [types]
+ Object
+ (toString [this]
+ (str (apply list 'I types))))
;; Type Constructors
+(declare massage-function-syntax normalise-tv-syntax tv-from-syntax)
+
(defmacro Fn [& arities]
- `(->Function
- (map arity-from-syntax ~(mapv massage-arity-syntax arities))))
+ `(apply I (map function-from-syntax ~(mapv massage-function-syntax arities))))
(defmacro All [tvars type]
- (let [normalised (normalise-tv-syntax tvars)
+ (let [normalised tvars
nmes (map first normalised)]
`(let [~@(mapcat vector nmes (map tv-from-syntax normalised))]
- (->PolyConstructorType (map tv-from-syntax ~normalised) ~type))))
+ (->PolyConstructorType ~(mapv tv-from-syntax normalised) ~type))))
(defn U [& types]
- (->UnionType types))
-
-(defn Case [& types]
- (->CaseType types))
+ (if (= 1 (count types))
+ (first types)
+ (->UnionType types)))
(defn I [& types]
- (->IntersectionType types))
+ (if (= 1 (count types))
+ (first types)
+ (->IntersectionType types)))
(defn Inst [this & types]
{:pre [(instance? PolyConstructorType this)]}
@@ -65,13 +84,17 @@
;; Syntax helpers
-(defn- massage-arity-syntax [arity-syntax]
- (replace {'& :& '-> :->} arity-syntax))
+(defn- massage-function-syntax [fun-syntax]
+ (replace {'& :& '-> :-> '* :*} fun-syntax))
-(defn arity-from-syntax [arity-syntax]
- (let [[dom rng] (split-with #(= :-> %) arity-syntax)
- [fixed-dom rest-dom] (split-with #(= :& %) dom)]
- (->Arity fixed-dom rng rest-dom)))
+;takes massaged syntax
+(defn function-from-syntax [fun-syntax]
+ (let [[dom [rng]] (split-with #(= :-> %) fun-syntax)
+ [fixed-dom rest-syn] (split-with #(= :& %) dom)
+ [has-uniform-rest uniform-rest]
+ (when (= ':* (last rest-syn))
+ [true (first rest-syn)])]
+ (->FunctionType fixed-dom rng has-uniform-rest uniform-rest)))
(def ^:private bound-syn :<)
@@ -81,43 +104,150 @@
bound (if (contains? opts bound-syn)
(bound-syn opts)
`Any)]
- `(->TV '~name ~bound ~variance)))
-
-;; Base types
-
-(def-type Any (U Object nil))
-(def-type Nothing (U))
-
-(def-type NonseqableSeqable
- (U Iterable
- ;array
- CharSequence
- java.util.Map))
+ `(->TV '~nme ~bound ~variance)))
+
+;; Type Protocols
+
+(defprotocol ITCType
+ "Marker protocol for all Typed Clojure types"
+ (-tctype-marker [this]))
+
+(defprotocol IPolyInst
+ "Marker protocol for polymorphic instances"
+ (-polyinst-marker [this]))
+
+(defprotocol IPolyConstructor
+ "Marker protocol for polymorphic type constructors"
+ (-polyconstructor-marker [this]))
+
+(defprotocol ISubtype
+ "Subtyping between ITCTypes"
+ (-subtype [this sup] "True if this is a subtype of sup"))
+
+(defprotocol IRuntimeClass
+ "Runtime class of ITCTypes"
+ (-runtime-class [this] "Returns the class representing this ITCType"))
+
+(defprotocol ISuperTypes
+ "Extract supertypes of an ITCType type"
+ (-supertype-of [this] "Returns the supertypes of an ITCType"))
+
+(defprotocol IInstanceOf
+ "Runtime predicates for ITCTypes"
+ (-instance-of [this v] "True if v is an instance of ITCType this"))
+
+;; Subtyping
+
+(defn tc-isa? [sub sup]
+ (cond
+ (and (instance? ISubtype sub)
+ (instance? ISubtype sup))
+ (-subtype sub sup)
+
+ (and (instance? IRuntimeClass sub)
+ (class? sup))
+ (isa? (-runtime-class sub) sup)
+
+ (and (class? sub)
+ (class? sup))
+ (isa? sub sup)
+
+ :else (throw (Exception. "no case in tc-isa?"))))
+
+(defn subtype? [sub sup]
+ (cond
+ (= Any sup) true
+ (instance? ISubtype sub) (-subtype sub sup)))
+
+(deftype Any []
+ ITCType
+ ISubtypesOf
+ (-supertype-of [this]
+ Any)
+ ISubType
+ (-subtype [this sup]
+ (identical? Any sup))
+ IInstanceOf
+ (-instance-of [this v]
+ true))
+
+(deftype Nothing []
+ ITCType
+ ISubtypesOf
+ (-supertype-of [this]
+ Any)
+ ISubType
+ (-subtype [this _]
+ true))
+
+(def-type EmptySeqable
+ Nothing)
+
+(def-poly-type NonEmptySeqable [[a :variance :covariant]]
+ Nothing)
(def-poly-type Seqable [[a :variance :covariant]]
- (U clojure.lang.Seqable
- NonseqableSeqable))
+ (U (NonEmptySeqable a)
+ EmptySeqable))
(def-poly-type Option [[a :variance :covariant]]
- (Case a
- nil))
+ (U a nil))
+
+(def-type EmptyColl
+ Nothing
+ :class clojure.lang.IPersistentCollection)
+
+(def-poly-type NonEmptyColl [[a :variance :covariant]]
+ Nothing
+ :class clojure.lang.IPersistentCollection)
(def-poly-type Coll [[a :variance :covariant]]
- (I clojure.lang.IPersistentCollection
- (Inst Seqable a)))
+ (I (U EmptyColl
+ (Inst NonEmpty a))
+ (Inst AnySeqable a))
+ :class clojure.lang.IPersistentCollection)
+
+(def-type EmptySeq
+ EmptySeqable
+ :class clojure.lang.ISeq)
+
+(def-poly-type NonEmptySeq [[a :variance :covariant]]
+ (Inst NonEmptySeqable a)
+ :class clojure.lang.ASeq)
(def-poly-type Seq [[a :variance :covariant]]
- (I clojure.lang.ASeq
+ (I (U EmptySeq
+ (Inst NonEmptySeq a))
(Inst Seqable a)
- (Inst Coll a)))
+ (Inst Coll a))
+ :class clojure.lang.ISeq)
+
+(def-type EmptyVector
+ EmptySeqable
+ :class clojure.lang.IPersistentVector)
-;; Subtype
+(def-poly-type NonEmptyVector [[a :variance :covariant]]
+ (Inst NonEmptySeqable a)
+ :class clojure.lang.IPersistentVector)
-(defmulti subtype (fn [type sup] [(class type) (class sup)]))
+(def-poly-type Vector [[a :variance :covariant]]
+ (I (U EmptyVector
+ (Inst NonEmptyVector a))
+ (Inst Seqable a)
+ (Inst Coll a))
+ :class clojure.lang.IPersistentVector)
+
+(+T clojure.core/seq
+ (All [[x :variance :covariant]]
+ (Fn [(EmptySeqable x) -> nil]
+ [(NonEmptySeqable x) -> (Seq x)]
+ [(Seqable x) -> (U (Seq x) nil)])))
-(defmethod subtype [Class Class]
- [type sup]
- (isa? type sup))
+(+T clojure.core/first
+ (All [[x :variance :covariant]]
+ (Fn [EmptySeqable -> nil]
+ [(NonEmptySeqable x) -> x]
+ [(Seqable x) -> (U x nil)])))
;; Checker
@@ -154,6 +284,8 @@
(assoc expr
type-key (-> cexprs last type-key))))
+(declare synthesise-type-args)
+
(defmethod check :invoke
[expr & [expected-type]]
(let [{cfexpr :fexpr
View
16 test/typed/test/example.clj
@@ -0,0 +1,16 @@
+(ns typed.test.example
+ (:require [typed.core :refer [+T def-type Fn Any All I U def-poly-type Inst Seqable
+ Seq]]))
+
+(def-type StringGenerator (Fn [& String -> String]))
+
+(def-poly-type SomePoly [[a :variance :invariant]
+ [b :variance :invariant]]
+ (Fn [& (Inst Seqable a) -> (Inst Seq b)]))
+
+(def-type Something (All [[x :< Object :variance :invariant]]
+ (Inst Seqable x)))
+
+(+T generate-string StringGenerator)
+(defn generate-string []
+ "a")
Please sign in to comment.
Something went wrong with that request. Please try again.