clojure-meetup-01-2019-dhall-demo.clj

(ns clojure-meetup.demo)


;; This is the main API of the package
;; - `input-ast` compiles the Dhall source, returns AST
;; - `input` also runs `eval` on the AST, so we get Clojure
(require '[dhall-clj.core :refer [input input-ast]])




;; As we saw, there are some amount of compiler phases.
;; We have a namespace for each one of them:

;; - parse
(require '[dhall-clj.parse :refer [parse expr]])

;; - resolve imports
(require '[dhall-clj.import :refer [resolve-imports]])
(require '[dhall-clj.state :as s])

;; - typecheck
(require '[dhall-clj.typecheck :refer [typecheck]])

;; - normalize/execute/reduce
(require '[dhall-clj.beta-normalize :refer [beta-normalize]])

;; - emit
(require '[dhall-clj.emit :refer [emit]])












;; Simple Dhall introduction in 30 seconds 🙌











;;; Dhall has Naturals, and we can add them up:
(input "1 + 1")


;; We can look at the type of our expression
(-> "1 + 1" parse expr (typecheck {}))








;; Dhall has a List type
(input "[1, 1, 2, 3, 5, 8]")


;; ..and we can do things like concat lists
(input "[13, 21] # [34]")









;; There is also a "map" type, called Record
(input "{ name = \"Clojure meetup\", year = 2019 }")


;; Let's ask for the type of it:
(-> "{ name = \"Clojure meetup\", year = 2019 }"
   parse
   expr
   (typecheck {}))


;; We can "merge" records
(input "{ foo = 42 } // { bar = True, bap = {=} }")







;; Unlike in Clojure, there is a "Maybe" type
;; and no strong feelings about it 😜
(input "Some 42")
(input "None Natural")





;; Let's not forget Booleans!
;; They are pretty important, as it's the only type
;; on which we can run stuff like "if/else"
(input "if True then 42 else 23")

;; And other things, like and/or
(input "True || False")








;; We can "let" things to assign them names
;; and we have a Text type that supports Unicode
;; and string interpolation!
(input "let name = \"Helsinki\" in \"Ciao ${name}! 🙌\"")









;st; Things get serious: we also have functions
(input "\\(n : Natural) -> n * 2")




;; We can actually run this in Clojure 😎
;; (also, fancy unicode!)
(let [twice (input "λ(n : Natural) → n * 2")]
  (twice 4))




;; But of course we can run stuff in Dhall-land as well
(input "let cube = λ(n : Natural) → n * n * n in cube 42")







;; OK, ready for a more interesting program?


;; Also, questions?








(input "

-- There are comments, unlike in JSON 😅

{-

And long comments too!

Here we take advantage of the safety of Dhall.
We have a local import (no http imports yet in dhall-clj!)
and we protect it with a hash.
If the file changes for some reason (because upgrade,
or some malicious user), Dhall will refuse to run our program.

Moreover, protected imports are cached, so next runs are faster.

Oh, and there is a standard library, called Prelude,
that implements a bunch of basic stuff on top of the
builtins.
-}

let map = ./dhall-lang/Prelude/List/map
  sha256:401176938d3a994be6664f89702f5d7a5146535a017da509eb477af78c2349bc

let cube = λ(n : Natural) → n * n * n

in map Natural Natural cube [ 1, 2, 3 ]
")











;; Alright, you are ready to code Dhall :)
















;; Now, let's see what happens in the different compiler phases




;; First, parsing

;; We use a super simple expression to demonstrate this
;; because it's going to be very verbose
(def source-simple "1")

;; This `parse` just does a very light processing on the
;; parse tree given by instaparse, which is VERY nested
(-> source-simple parse)



;; This is not actually useful until we convert it to AST
;; To convert it from enlive-style-tree to AST we use `expr`
(-> source-simple parse expr)










;; Next up, we have to run the import resolution code
;; that finds the imports in the AST and replaces them with
;; the AST of the imported expressions
;; Let's use the `map` from the Prelude to demonstrate:
(def source' "./dhall-lang/Prelude/List/map")

(-> source' parse expr (resolve-imports (s/new)))










;; Next, typecheck. This verifies that our AST is a "valid" program
;; E.g. if we have a function that takes a Natural and we pass a Bool
;; the typecheck will fail

(def source-type-error "(λ(x : Natural) → x) True")

(-> source-type-error parse expr (typecheck {}))




;; If everything is fine, typecheck returns the type

(def source "(λ(x : Natural) → x) 42")

(-> source parse expr (typecheck {}))







;; Once we're sure that our program typechecks
;; (so it's a valid program), we can run it

;; Note: skipping import resolution here, as we don't have imports
(let [ast (-> source parse expr)
      _type (typecheck ast {})]
  (beta-normalize ast))



;; The above is basically what `input-ast` does





;; Additionally to that, `input` also evaluates
;; to Clojure

;; We can actually see the Clojure code being generated
;; with `emit`

(let [source "λ(x : Natural) → x + 1"
      ast (-> source parse expr)
      _type (typecheck ast {})]
  (-> ast beta-normalize emit))






;; That's it :)









;; USECASE: it's pretty cool that we can SAFELY throw code on the wire

(def source "λ(version : Natural) → { version = \"${Natural/show version}.0\" }")


;; Import the binary protocol stuff
(require '[dhall-clj.binary :refer [encode decode]])


;; This will be a byte-array
(def serialized (-> source input-ast encode))

(type serialized)

(vec serialized)



;; ...now, you can send these bytes to another machine
;; (literally on the wire)


;; Once there, you can deserialize and run this function

(def make-version (-> serialized decode emit eval))

(type make-version)

(make-version 2)