Skip to content

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
...
  • 2 commits
  • 3 files changed
  • 0 commit comments
  • 1 contributor
View
9 articles/ecosystem/core_typed/home.md
@@ -32,12 +32,14 @@ We discuss some theory and design goals of core.typed.
### [Annotations](start/annotations.html)
-Where and how to annotate your code to help core.typed.
+Where and how to annotate your code to help core.typed check your code.
### [Types](types.html)
Syntax and descriptions of core.typed types.
+### [Polymorphic Functions, Bounds and Higher-kinded Variables](poly_fn.html)
+
### [Filters](filters.html)
An overview of filters for occurrence typing.
@@ -46,10 +48,11 @@ An overview of filters for occurrence typing.
Typing definitions and usages of Clojure datatypes and protocols.
-### Multimethods
+### [Looping constructs](loops.html)
+
+core.typed provides several wrapper macros for common looping constructs.
### Dotted Functions
-### Polymorphism, Variance and F-Bounds
### Java Classes, Arrays and Interop
## Miscellaneous Tutorials
View
55 articles/ecosystem/core_typed/loops.md
@@ -0,0 +1,55 @@
+---
+title: "Looping constructs"
+layout: article
+---
+
+Due to limitations in core.typed's inference, we require using "typed" versions
+of several core forms.
+
+# loop
+
+Usages of `loop` should be replaced with `clojure.core.typed/loop>`.
+
+The syntax is identical except each loop variable requires a type annotation.
+
+```clojure
+(loop> [[a :- Number] 1
+ [b :- (U nil Number)] nil]
+ ...)
+```
+
+# Named fn's
+
+Named `fn`'s require full annotation for accurate recursive calls inside the `fn` body.
+
+```clojure
+clojure.core.typed=> (cf (ann-form (fn a [n] (+ (a 1) n))
+ [Number -> Number]))
+(Fn [java.lang.Number -> java.lang.Number])
+```
+
+# for
+
+Use `clojure.core.typed/for>` instead of `for`.
+
+`for>` requires annotations for the return type of the body
+of the for, and the left hand side of each binding form.
+
+```clojure
+(for> :- Number
+ [[a :- (U nil AnyInteger)] [1 nil 2 3]
+ :when a]
+ (inc a))
+```
+
+# doseq
+
+Use `clojure.core.typed/doseq>` instead of `doseq`.
+
+`doseq>` requires annotations for the left hand side of each binding form.
+
+```clojure
+(doseq> [[a :- (U nil AnyInteger)] [1 nil 2 3]
+ :when a]
+ (inc a))
+```
View
88 articles/ecosystem/core_typed/poly_fn.md
@@ -0,0 +1,88 @@
+---
+title: "Polymorphic Functions"
+layout: article
+---
+
+core.typed supports polymorphic function types. They allow us to specify
+function types which are both general and accurate.
+
+# All
+
+The primitive `All` constructor creates a polymorphic binder and scopes
+type variables in a type.
+
+The identity function has a simple polymorphic type:
+
+```clojure
+(All [x]
+ [x -> x])
+```
+
+Read: for all types `x`, a function that takes an `x` and returns an `x`.
+
+Polymorphic types are introduced with annotations, but where are they eliminated?
+We use local type inference to infer type variable types based on how they are used.
+
+```clojure
+(identity :a)
+```
+
+In the above example, we infer `x` to be `Keyword`, and instantiate the polymorphic
+type as `[Keyword -> Keyword]`.
+
+## Bounds
+
+Type variables support upper and lower type bounds, which default to `Any` and `Nothing`
+respectively.
+
+Equivalently, the type:
+
+```clojure
+(All [x] ...)
+```
+
+is shorthand for:
+
+```clojure
+(All [[x :> Nothing :< Any]] ...)
+```
+
+We use bounds to ensure a type variable can only be instantiated to a particular type.
+
+The type of an identity function that only accepts `Number`s can be written:
+
+```clojure
+(All [[x :< Number]]
+ [x -> x])
+```
+
+Bounds do not seem as useful in core.typed as languages like Java or Scala.
+Often, combinations of ordered function intersections and unions are more useful.
+
+Bounds are also recursive: a bound can refer to the variable it's bounding.
+Type variables to the left of the type variable being bounded in the same binder are in scope in a bound.
+
+## Higher-kinded variables
+
+Note: Experimental feature
+
+A type variable can be of a higher-kind.
+
+```clojure
+(def-alias AnyMonad
+ (TFn [[m :kind (TFn [[x :variance :covariant]] Any)]]
+ '{:m-bind (All [x y]
+ [(m x) [x -> (m y)] -> (m y)])
+ :m-result (All [x]
+ [x -> (m x)])
+ :m-zero (U (All [x] (m x)) Undefined)
+ :m-plus (U (All [x]
+ [(m x) * -> (m x)])
+ Undefined)}))
+```
+
+In this type, `x` is a type function taking a type and returning a type.
+For those familiar with Haskell, `x` is of kind `* -> *`.
+
+The type function is also covariant, which further ensures `x` is instantiated
+to a covariant type function.

No commit comments for this range

Something went wrong with that request. Please try again.