frenchy64

Occurrence Typing is Compositional

A few months ago, Sam Tobin-Hochstadt explained to me how occurrence typing is compositional. While I had taken this for granted previously, comparing occurrence typing to other systems makes it clear that this is an important property to have.

First of all, what is occurrence typing? In dynamically typed programs, there are often type invariants enforced at program branches.

(fn [a :- (U nil String)]
  (if a
 (count a)

frenchy64

(ns typed.core
  (:require [clojure.core.typed :as t]))

(t/ann-datatype Foo [fooName :- t/Str])
(deftype Foo [fooName])

(t/ann-datatype Bar [barName :- t/Str])
(deftype Bar [barName])

(t/ann theName [(t/U Foo Bar) -> t/Str])

frenchy64

Clojure 1.7.0-beta1
Reflection warning, /tmp/form-init8630209280621436300.clj:1:1389 - reference to field ns can't be resolved.
Reflection warning, /tmp/form-init8630209280621436300.clj:1:3631 - reference to field name can't be resolved.
    Docs: (doc function-name-here)
          (find-doc "part-of-name-here")
  Source: (source function-name-here)
 Javadoc: (javadoc java-object-or-class-here)
    Exit: Control+D or (exit) or (quit)
 Results: Stored in vars *1, *2, *3, an exception in *e

frenchy64

nREPL server started on port 64499 on host 127.0.0.1 - nrepl://127.0.0.1:64499
REPL-y 0.3.1
Clojure 1.7.0-alpha6
Reflection warning, /tmp/form-init8946539659736038022.clj:1:1389 - reference to field ns can't be resolved.
Reflection warning, /tmp/form-init8946539659736038022.clj:1:3631 - reference to field name can't be resolved.
    Docs: (doc function-name-here)
          (find-doc "part-of-name-here")
  Source: (source function-name-here)
 Javadoc: (javadoc java-object-or-class-here)
    Exit: Control+D or (exit) or (quit)

frenchy64

destruct takes a term of inductive type (or co-inductive, whatever that is), and generates the number of goals equal to the different ways this term can be constructed.

destruct term as [c H] is a nice trick if term is an existential. ex_intro is the only constructor of ex:

ex_intro : forall x:A, P x -> ex (A:=A) P.

This way destruct chooses a variable for the existential, and also calls it c and the body of the existential H.

frenchy64

Transient semantics for gradual typing avoids proxies and adds defensive checks.

(ns gt.t
  (:require [clojure.core.typed :as t]
            [gt.u2]))
  
(t/ann +1 [t/Num -> t/Num])
(defn +1 [a] (inc a))
;(defn +1 [a] (inc (t/cast a Num)))

frenchy64

(defmacro assoc-in*
  "Associates a value in a nested associative structure, where ks is a
  sequence of keys and v is the new value and returns a new nested structure.
  If any levels do not exist, hash-maps will be created."
  {:added "1.0"
   :static true}
  [m [k & ks] v]
  (if ks
    `(let [m# ~m k# ~k] (assoc m# k# (assoc-in* (get m# k#) ~ks ~v)))
    `(assoc ~m ~k ~v)))

frenchy64

> (run 10 (q)
    (infer '() q 'num '(not (val #f) x) '(is (val #f) x) empty-object))

((ann _.0 num ff ff empty) 
 (ann _.0 (U) ff ff empty)
 ((ann _.0 (val _.1) ff ff empty) (num _.1)) 
 (ann _.0 num ff ff empty) 
 (ann _.0 num ff (is (val #f) x) empty) 
 (ann _.0 num ff (is (U) x) empty) 
 (ann _.0 num ff (is (U (val #f) (val #f)) x) empty) 

frenchy64

#lang racket

(require "mk/mk.rkt")

(define-syntax test
  (syntax-rules ()
    ((_ title tested-expression expected-result)
     (begin
       (printf "Testing ~s\n" title)
       (let* ((expected expected-result)

frenchy64

(ns demo.core
  (:require [clojure.core.typed :as t]))
  
;; Map vs Vector AST representation

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; * Maps 

(t/defalias M (t/U '{:op ':if :test M :then M :else M}
                   '{:op ':do :e1 M :e2 M}