『型システムのしくみ』(Type Systems Distilled with TypeScript) type checker implementations in Clojure

arith.clj

(ns arith
  (:require
   [clojure.spec.alpha :as s]))

;;; definition of terms
;;; <term> ::= true
;;;          | false
;;;          | (if <term> <term> <term>)
;;;          | <number>
;;;          | (+ <term>*)

(declare term-tag-spec)
(s/def :term/tag #{:true :false :if :number :+})
(s/def :term/term (s/multi-spec term-tag-spec :term/tag))

(s/def :if/cond :term/term)
(s/def :if/then :term/term)
(s/def :if/else :term/term)

(s/def :number/n number?)

(s/def :+/args (s/* :term/term))

(defmulti term-tag-spec :term/tag)

(defmethod term-tag-spec :true [_]
  (s/keys :req [:term/tag]))

(defmethod term-tag-spec :false [_]
  (s/keys :req [:term/tag]))

(defmethod term-tag-spec :if [_]
  (s/keys :req [:term/tag :if/cond :if/then :if/else]))

(defmethod term-tag-spec :number [_]
  (s/keys :req [:term/tag :number/n]))

(defmethod term-tag-spec :+ [_]
  (s/keys :req [:term/tag :+/args]))

(comment
  (s/valid? :term/term #:term{:tag :if
                              :if/cond #:term{:tag :true}
                              :if/then #:term{:tag :number
                                              :number/n 1}
                              :if/else #:term{:tag :false}})

  (s/valid? :term/term #:term{:tag :+ :+/args [#:term{:tag :number
                                                      :number/n 1}
                                               #:term{:tag :number
                                                      :number/n 2}]})
  )

;;; parser from s-expressions to terms

(defn- if-expr? [sexp]
  (and (list? sexp)
       (= (first sexp) 'if)
       (= (count sexp) 4)))

(defn- +-expr? [sexp]
  (and (list? sexp)
       (= (first sexp) '+)
       (pos? (count sexp))))

(s/fdef parse
  :args (s/cat :sexp any?)
  :ret :term/term)

(defn parse [sexp]
  (cond
    (true? sexp) #:term{:tag :true}
    (false? sexp) #:term{:tag :false}
    (if-expr? sexp) (let [[cond then else]
                          (->> sexp rest (mapv parse))]
                      #:term{:tag :if
                             :if/cond cond
                             :if/then then
                             :if/else else})
    (number? sexp) #:term {:tag :number
                           :number/n sexp}
    (+-expr? sexp) (let [args (->> sexp rest (mapv parse))]
                     #:term{:tag :+
                            :+/args args})
    :else (throw (ex-info "Parse error" {:sexp sexp}))))

(comment
  (s/valid? :term/term (parse '(if true 1 (+ 2 (if false 3 4)))))

  (s/valid? :term/term (parse (read-string "(if true 1 (+ 2 (if false 3 4)))")))
  )

;;; definition of types
;;; <Type> ::= Boolean | Number

(s/def :type/tag #{:boolean :number})
(s/def :type/type (s/keys :req [:type/tag]))

;;; type checker

(s/fdef type-check
  :args (s/cat :term :term/term)
  :ret :type/type)

(defmulti type-check :term/tag)

(defmethod type-check :true [_] #:type{:tag :boolean})

(defmethod type-check :false [_] #:type{:tag :boolean})

(defmethod type-check :if [{:if/keys [cond then else] :as term}]
  (let [cond-type (type-check cond)
        then-type (type-check then)
        else-type (type-check else)]
    (when (not= (:type/tag cond-type) :boolean)
      (throw (ex-info "Type error in if expression: boolean expected" {:term term})))
    (when (not= then-type else-type)
      (throw (ex-info "Type error in if expression: then and else have different types" {:term term})))
    then-type))

(defmethod type-check :number [_] #:type{:tag :number})

(defmethod type-check :+ [{:+/keys [args] :as term}]
  (let [arg-types (map type-check args)]
    (when (some #(not= (:type/tag %) :number) arg-types)
      (throw (ex-info "Type error in + expression: numbers expected" {:term term})))
    #:type{:tag :number}))

(comment
  (require '[clojure.spec.test.alpha :as st])
  (st/instrument `type-check)

  (type-check (parse '(if true 1 (+ 2 (if false 3 4)))))

  (type-check (parse '(if 5 1 (+ 2 (if false 3 4)))))

  (type-check (parse '(if true false (+ 2 (if false 3 4)))))

  (type-check (parse '(if true 1 (+ 2 (if false 3 4) false))))
  )

ref. https://github.com/LambdaNote/support-ts-tapl/tree/main/book/typecheckers