Forem: 林子篆

A wrong question: Is a Square a Rectangle?

林子篆 — Mon, 16 Nov 2020 00:00:00 +0000

Overview

what is Subtyping?
what is Liskov Substitution Principle?
what's the problem?
how to solve this mistake of type system

What is Subtyping?

A common misunderstanding is OOP must have subtyping and generic at the same time, but they are independent features, generic is just a type-level function with takes a type, generates a type. Subtyping is a relationship between type, when we say A <: B, which means A is a subtype of B. In Java, we use concrete syntax extends or implements.

What is Liskov Substitution Principle(LSP)?

LSP said

if S is a subtype of T, then objects of type T in a program may be replaced with objects of type S without altering the program

What's the problem

Square is a special Rectangle where all four sides are equal in length. Thus we might write down:

public class Rectangle {
    double x, y;
    Rectangle(double initX, double initY) { x = initX; y = initY; }

    public void setX(double x) { this.x = x; }
    public void setY(double y) { this.y = y; }
}

class Square extends Rectangle {
    Square(double initX, double initY) throws SquareException {
        super(initX, initY);
        if (initX != initY) {
            throw new SquareException(initX, initY);
        }
    }
}

Ok, so we can have following program:

Square s = new Square(2, 2);
Rectangle r = s;
r.setX(10);

Oops, s is not a square anymore, this correctly follows LSP but incorrect generally.

Solution

Here is a solution: refinement type. By using refinement type, we can claim type Square = Rectangle when (x = y). Then problem solved, when programming if we can't proof x = y this predicate then compiler won't think that is a Square but a Rectangle. Since Square is a Rectangle, method in Rectangle still can be using by Square, thus we didn't lose our power. However, program like s.setX(v), would need to prove v = y, to prove it is a Square. Here we have two choices:

change s type to Rectangle, the problem of this solution is if we write r = s; r.setX(v), compiler might not work for this(this is also why I'm designing controllable-refinement), mutable semantic always needs more effort.
throw compile error that Square constraint was broke by the statement.

Choose one and work with it, that's all, have a nice day.

How to find mk fixed point

林子篆 — Sun, 26 Jul 2020 00:00:00 +0000

This article is about how to get a fixed point in lambda calculus(utlc) system, if you didn't familiar with it, you can read NOTE: what is lambda calculus to get start. What's a fixed point? When a function f(x)f(x)f(x) has xxx can make f(x)=xf(x) = xf(x)=x then we say xxx is the fixed point of fff. Now we can get start to derive one.

In lambda calculus, Peano's number can be represented as:

z: λs.λz.z\lambda s . \lambda z . zλs.λz.z
s z: λs.λz.s z\lambda s . \lambda z . s \; zλs.λz.sz
s s z: λs.λz.s (s z)\lambda s . \lambda z . s \; (s \; z)λs.λz.s(sz)

Then s (successor) can be found.

s≐λn.λs.λz.s (n s z)s \doteq \lambda n . \lambda s . \lambda z . s \; (n \; s \; z)s≐λn.λs.λz.s(nsz)

With s , we can define add , idea is simple: find number nnn successor of mmm.

add≐λn.λm.m (s n)add \doteq \lambda n . \lambda m . m \; (s \; n)add≐λn.λm.m(sn)

We can check a number is zero or not(assume true/false already defined) and predecessor.

iszero≐λn.n (λx.false) truepredecessor≐λn.λs.λz.second (n (wrap f)<true,x>)wrapf≐λp.<false,if (first p) (second p) (f (second p))>iszero \doteq \lambda n . n \; (\lambda x . false) \; true \
predecessor \doteq \lambda n . \lambda s . \lambda z . second \; (n \; (wrap \; f) <true, x>) \
wrap f \doteq \lambda p . <false, if \; (first \; p) \; (second \; p) \; (f \; (second \; p))>iszero≐λn.n(λx.false)truepredecessor≐λn.λs.λz.second(n(wrapf))wrapf≐λp.

p.s. represents a pair, first is a, and second is b. Assuming first and second already bound.

With these, we can define mult

mult≐λn.λm.if (iszero n) 0 (add m (mult (predecessor n) m))mult \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; (mult \; (predecessor \; n) \; m))mult≐λn.λm.if(iszeron)0(addm(mult(predecessorn)m))

However, lambda didn't have a name(all ≐\doteq≐ was name tag for human only, not allowed in lambda calculus), so we cannot refer to mult in mult! But we can have a proper version.

mkmult≐λn.λm.if (iszero n) 0 (add m ((t t) (predecessor n) m))mkmult \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; ((t \; t) \; (predecessor \; n) \; m))mkmult≐λn.λm.if(iszeron)0(addm((tt)(predecessorn)m))

How to use this?

mult≐(mkmult mkmult)mult \doteq (mkmult \; mkmult)mult≐(mkmultmkmult)

The key was a recursively expanded definition for mult. t t always take a mkmult and make more mkmult. Thus, can we generalize this?

mk≐λt.t(mk t)mk \doteq \lambda t . t (mk \; t)mk≐λt.t(mkt)

Oops, but wait, we can repeat the pattern.

mkmk≐λk.λt.t ((k k) t)mkmk \doteq \lambda k . \lambda t . t \; ((k \; k) \; t)mkmk≐λk.λt.t((kk)t)

Then we have mk, for sure.

mk≐(mkmk mkmk)mk \doteq (mkmk \; mkmk)mk≐(mkmkmkmk)

With mk we can have mult by a different way.

mkmult′≐λn.λm.if (iszero n) 0 (add m (t (predecessor n) m))mult≐(mkmkmult′)mkmult' \doteq \lambda n . \lambda m . if \; (iszero \; n) \; 0 \; (add \; m \; (t \; (predecessor \; n) \; m))
mult \doteq (mk mkmult')mkmult′≐λn.λm.if(iszeron)0(addm(t(predecessorn)m))mult≐(mkmkmult′)

mk can find out fixed point of any function. Which means M (mk M) = (mk M). mk is not the only fixed point, the most famous fixed point is Y combinator, but I'm not going to talk about it here. At the end, thanks for the read and have a nice day.

Hindley-Milner type system: Incrementally build way & Make new language in Racket

林子篆 — Sun, 24 May 2020 00:00:00 +0000

Hindley-Milner (HM) type system is a classical type system for lambda calculus with parametric polymorphism. Its most notable property is it can infer most types of a given program, without type annotations! However, this feature sounds cool but not work well in practice XD, since people need annotation to hint ourselves when reading. I pick this system as a topic is because the HM type system probably is the easiest completeness system with parametric polymorphism. It's a good start for understanding other more complex type systems, and it's important for gradual typing. But before we dig too deep into those ideas, let's start to understand HM, the point of this article.

Why?

In earlier days Lisp didn't have a type system, as time pass, people start to want to(or need to) express program more precisely since cooperation and robustness. Then people start working for their needs. To express a list, introduce parametric polymorphism. parametric polymorphism sounds scared but doesn't, let's view an example:

(: list-length (All (A) (-> (Listof A) Integer)))

This syntax bind list-length to a type (All (A) (-> (List A) Integer)), or we would write list-length : (All (A) (-> (List A) Integer))(you can see Racket use prefix operator, very Lisp style, not surprise XD). The syntax is not the most important thing, but it shows a very common thing in many different languages, to help you get what is parametric polymorphism. Now imagine, every time call list-length, must provide A as an argument: (list-length Number lst). People would get tired and say: I hate the static type system, it seems no surprise. That's the reason for type inference. With type inference, if lst : (Listof Number), A is Number, get type without type! The idea is so frustrating and makes people crazy to think about: Can we have a system, get all the type without type? The result is the HM type system.

Why Polymorphism

In simply typed lambda calculus (STLC), asking e : T make sense because we already give e a type K, check T is K is all we need. All type in STLC is a T or T -> T and T will not from another type. This feature, however, makes inconvenience when writing a program, for example:

(define id
  (lambda (x) x))

Identity function can work well with any type, but now we have to provide infinite versions for it:

(: id-str (-> str str))
(define id-str (lambda (x) x))
(: id-int (-> int int))
(define id-int (lambda (x) x))
(: id-bool (-> bool bool))
(define id-bool (lambda (x) x))
(: id-int-to-int (-> (-> int int) (-> int int)))
(define id-int-to-int (lambda (x) x))

If I don't want it and still want types, then use polymorphism is the solution:

(: id (All (A) (-> A A)))
(define id
  (lambda (x) x))

I hope I convince you that, take your time to understand its detail of this system is valuable :).

Setup a project

This section helps you get a project would be modified in the following part:

raco pkg new hindley-milner
cd hindley-milner
raco pkg install --auto

Syntax Overview

I would show a small enough language can cooperate with HM type system and big enough to convince you this is useful, detail would not be the point, put them at here is just want to help you keep going with the following content.

Definition of language(create lang.rkt):

#lang typed/racket

(provide expr expr:int expr:bool expr:string expr:list expr:variable expr:lambda expr:application expr:let)

(struct expr [] #:transparent)
(struct expr:int expr [(v : Integer)] #:transparent)
(struct expr:bool expr [(v : Boolean)] #:transparent)
(struct expr:string expr [(v : String)] #:transparent)
(struct expr:list expr [(elems : (Listof expr))] #:transparent)
(struct expr:variable expr [(name : String)] #:transparent)
(struct expr:lambda expr
  [(param : (Listof String))
   (body : expr)]
  #:transparent)
(struct expr:application expr
  [(func : expr)
   (args : (Listof expr))]
  #:transparent)
(struct expr:let expr
  [(bindings : (Listof (Pair String expr)))
   (expr : expr)]
  #:transparent)

Definition of types(create typ.rkt)

#lang typed/racket

(provide typ typ:builtin)

(struct typ [] #:transparent)
(struct typ:builtin typ
  [(name : String)]
  #:transparent)

I will not explain them immediately, but let our incrementally steps show the story, let's start the journey.

Part I: Incrementally build up inference

Then we learn how to incrementally build up the HM type system without memorizing all rules. It also shows how to get ideas behind rules, not just remember a snapshot!

Monomorphism stuff

Monomorphism, which means obviously and decidable, and it would be a good start. Here, code can explain it better(create semantic.rkt):

#lang typed/racket

(provide type/infer)

(require "lang.rkt"
         "typ.rkt")

(: type/infer (-> expr typ))
(define (type/infer exp)
  (match exp
    ([expr:int _] (typ:builtin "int"))
    ([expr:bool _] (typ:builtin "bool"))
    ([expr:string _] (typ:builtin "string"))))

You can see why I say they are obviously even you never use static type, because this type is builtin in most language, inference their types is just by definition. 1 is int, #t is bool, "hello" is string. However, there has a common builtin type is not monomorphism, for example: list.

List

The inference list type is not that easy, because it's a type depends on the type, what's that mean? It means we say: list A is a type when A is a type, so must have a type A to have type list A, this called type depends on the type. This means, if we want to inference type of list, we also need to inference the type of its element and check rest elements following the same type. An edge case is somehow, some lists do not contain any element, in such case we still need a type, so we give it a placeholder of the type usually called free type variable(freevar). Finally, returns a type list with its type of argument. You can try to build it by yourself, but you would find there is something missing and became a wall stop you. The first thing we need to do, is extending our type definition to fit a type with type parameter this abstraction(modify typ.rkt):

(struct typ:freevar typ
  [(index : Integer)]
  #:transparent)
(struct typ:constructor typ
  [(name : String)
   (arg : (Listof typ))]
  #:transparent)
(: typ:builtin (-> String typ:constructor))
(define (typ:builtin name)
  (typ:constructor name '()))

Now typ:builtin is just a special case of typ:constructor, and we introduce the placeholder: typ:freevar. The second thing need to prepare is Context(modify semantic.rkt, put them before type/infer), which maintaining the state of freevar counting:

(struct Context
  [(freevar-counter : Integer)]
  #:transparent
  #:mutable)
(: Context/new (-> Context))
(define (Context/new)
  (Context 0))
(: Context/new-freevar! (-> Context typ))
(define (Context/new-freevar! ctx)
  (let ([cur-count (Context-freevar-counter ctx)])
    (set-Context-freevar-counter! ctx (+ 1 (Context-freevar-counter ctx)))
    (typ:freevar cur-count #f)))

Then we can start adding inference of expr:list:

(: unify (-> typ typ Void))
(define (unify t1 t2)
  (match (cons t1 t2)
    ([cons (typ:constructor a al) (typ:constructor b bl)]
     #:when (string=? a b)
     (for-each (λ ((ae : typ) (be : typ))
                 (unify ae be))
               al bl))
    (_ (raise (format "cannot unify type ~a and ~a" t1 t2)))))

; ->* is a special type, which means `->* list-of-required-parameters list-of-optional-parameters return-type`
(: type/infer (->* (expr) (Context) typ))
(define (type/infer exp)
  (match exp
    ; ignore
    ([expr:string _] (typ:builtin "string"))
    ([expr:list elems]
     (typ:constructor "list"
                      (list (if (empty? elems)
                        (Context/new-freevar! ctx)
                        ; use first element type as type of all elements
                        (let ([elem-typ (type/infer (car elems))]) ; (car (list 1 2 3)) is 1
                          ; check all elements follow first element type
                          (for-each (λ ([elem : expr]) (unify elem-typ (type/infer elem)))
                            (cdr elems)) ; (cdr (list 1 2 3)) is (list 2 3)
                          elem-typ)))))))

Currently, unify just check two constructors has the same name, and keep unify their parameters if has. In other cases, throw an exception.

Variable

A variable would have a type, or it binds with a type. Anyway, that means we can infer the type of variable, but we need a place to store this information. Therefore, a new abstraction introduced Environment(modify semantic.rkt, put code before Context):

(struct Env
  [(parent : (Option Env))
   (type-env : (Mutable-HashTable String typ))]
  #:transparent
  #:mutable)
(: Env/new (->* () ((Option Env)) Env))
(define (Env/new [parent #f])
  (Env parent (make-hash '())))
;;; Env/lookup take variable name such as `x` to get a type from env
(: Env/lookup (-> Env String typ))
(define (Env/lookup env var-name)
  (: lookup-parent (-> typ))
  (define lookup-parent (λ ()
                          (: parent (Option Env))
                          (define parent (Env-parent env))
                          (if parent
                              ; dispatch to parent if we have one
                              (Env/lookup parent var-name)
                              ; really fail if we have no parent environment
                              (raise (format "no variable named: `~a`" var-name)))))
  ; try to get value from table
  (let ([typ-env : (Mutable-HashTable String typ) (Env-type-env env)])
    (hash-ref typ-env var-name
              ; if fail, handler would take
              lookup-parent)))

then add a new field into Context:

(struct Context
  [(freevar-counter : Integer)
   (type-env : Env)]
  #:transparent
  #:mutable)
(: Context/new (-> Context))
(define (Context/new)
  (Context 0 (Env/new)))

Now we can get the variable type from Context:

(: type/infer (->* (expr) (Context) typ))
    ; ignore
    ([expr:variable name] (Env/lookup (Context-type-env ctx) name))

Wait, we use variable then must somewhere we define it, where is it? Therefore, the next section is lambda, lambda would introduce new variables into the environment.

Lambda

Things are getting more complex, get really to understand what we need to do? Lambda in the HM system well not have type annotation for parameters, it causes the same problem just like what list gives us. This means we need to bind a freevar with parameters as variables into a new environment. At here, since the multiple parameters are valid in this language, I introduce type pair to abstraction on this rather than extend type definition. Then, we use this new environment to infer the type of body, and produce arrow type(If you don't understand arrow type, I suggest you read STLC for explanation) via the inferred result. Now, it's time for some program:

Bind variable

(: Env/bind-var (-> Env String typ Void))
(define (Env/bind-var env var-name typ)
  (let ([env (Env-type-env env)])
    (if (hash-has-key? env var-name)
        (raise (format "redefined: `~a`" var-name))
        (hash-set! env var-name typ))))

Infer

(: type/infer (->* (expr) (Context) typ))
    ; ignore
    ([expr:lambda params body]
     ; params use new freevars as their type
     (letrec ([λ-env : Env (Env/new (Context-type-env ctx))]
           [param-types (typ:constructor
                         "pair"
                         (map (λ ([param-name : String])
                                (let ([r (Context/new-freevar! ctx)])
                                  (Env/bind-var λ-env param-name r)
                                  r)) params))])
       (set-Context-type-env! ctx λ-env)
       (define body-typ (type/infer body ctx))
       (typ:arrow param-types body-typ)))

WARN: notice since I always invoke type/infer without context in outside, type-env no need to set back to the original one. However, if you extend this language with define such sharing Context, then set environment back is required, else your local bindings would affect the outer scope.

Lambda seems powerful, and let can be translated to lambda, right? Unfortunately, it's correct in the computation view, but incorrect in the inference view. For example:

((λ (id) (id 1)) (λ (a) a))

It gets an identity function and applies to 1, it seems like it should get int. However, we would get a freevar. Because no one requires id start infer its type since we have no idea when would lambda apply to something, if remove (λ (a) a) and application form outside of (λ (id) (id 1)), we cannot ensure the type of (id 1). That's what let polymorphism going to solve.

Let polymorphism

Let polymorphism is the key expression in the HM type system, which ensures inference is decidable. The problem in the previous section can be fixed if using let:

(let ([id (λ (a) a)])
  (id 1))

Because let would infer the type of id immediately. Then the problem would be eliminated. So the only different part between let and lambda, is let bind its variable with inferred type, not freevar:

(: type/infer (->* (expr) (Context) typ))
    ; ignore
    ([expr:let bindings exp]
     (letrec ([let-env : Env (Env/new (Context-type-env ctx))]
              [bind-to-context (λ ([bind : (Pairof String expr)])
                                 (match bind
                                   ([cons name init]
                                    (Env/bind-var let-env name (type/infer init ctx)))))])
       (map bind-to-context bindings)
       (set-Context-type-env! ctx let-env)
       (type/infer exp ctx)))

Finally, we came to infer the last expression: expr:application.

Application

Infer application needs to do a few checks:

For application (func args ...), infer the type of func.
Check type of func is a arrow type: A -> B.
Assume return type is a freevar.
Unify A -> B with (typeof (args ...)) -> freevar.
return freevar as infer result.

With the explanation, we can start coding:

(: type/infer (->* (expr) (Context) typ))
    ; ignore
    ([expr:application fn args]
     (let ([fn-typ (type/infer fn ctx)]
           [args-typ (map (λ ((arg : expr)) (type/infer arg ctx)) args)]
           [fresh (Context/new-freevar! ctx)])
       (unify fn-typ (typ:arrow (typ:constructor "pair" args-typ) fresh))
       fresh))
  ; don't forget to close parenthesis!
  ))

We almost complete, but we have new jobs in unify to do since application might unify freevar and arrow type now.

Unify freevar

(: unify (-> typ typ Void))
(define (unify t1 t2)
  (match (cons t1 t2)
    ; ignore
    ([cons (typ:arrow p1 r1) (typ:arrow p2 r2)]
     (unify p1 p2)
     (unify r1 r2))
    ;;; freevar type is only important thing in `unify` function
    ((and
      [cons _ (typ:freevar _ _)]
      [cons t v])
     (if (or (eqv? v t) (not (occurs v t)))
         (subst! v t)
         (void))
     (void))
    ([cons (typ:freevar _ _) t2] (unify t2 t1))
    ; ignore
    ))

Unify arrow type is simple, in fact, we can totally replace typ:arrow with typ:constructor XD. In fact, all type constructors can be unify in the same way. freevar brings a new thing: occurs, what's occurs?

Occurs check

Occurs check make unification fail when unify V and T, T contains V. If we didn't do this check, unify would lead to unsound inference, for example:

(= ?0 (list ?0))

What would ?0 be? It would cause an infinite loop at there: (list (list (list ...))). Therefore, we need to check if V occurs in T:

(: occurs (-> typ typ Boolean))
(define (occurs v t)
  (match (cons v t)
    ; same freevar means `v` occurs in `t`, then should be rejected
    ([cons v (typ:freevar _ _)] (eqv? v t))
    ; arrow and constructor both just keep check on type parameters
    ([cons v (typ:arrow t1 t2)] (or (occurs v t1) (occurs v t2)))
    ([cons v (typ:constructor _ type-params)]
     (foldl (λ ([t : typ] [pre-bool : Boolean])
              (or pre-bool (occurs v t)))
            #f
            type-params))
    ; rest is fine
    (_ false)))

Now, the whole inference part done, if you want to know how to build a new language in Racket then keep going, or you can close the tab now XD.

Part Two: Make new language in Racket

After we build up a type system, we definitely want to see it work as a language, and make a new language in Racket is crazy easy! Let's start the second part.

Pretty Print

First, to improve readability, we need pretty-print function(create pretty-print.rkt):

#lang typed/racket

(require "typ.rkt")

(provide pretty-print-typ)

(: pretty-print-typ (-> typ String))
(define (pretty-print-typ t)
  (match t
    ([typ:freevar idx subst]
     (if subst
         (pretty-print-typ subst)
         (format "?~a" idx)))
    ([typ:constructor name typ-args]
     (if (empty? typ-args)
         (format "~a" name)
         (let ([j (string-join (map
                                (λ ([typ-arg : typ])
                                  (pretty-print-typ typ-arg))
                                typ-args) " ")])
           (if (string=? name "pair")
               (format "(~a)" j)
               (format "(~a ~a)" name j)))))
    ([typ:arrow from to]
     (format "~a -> ~a" (pretty-print-typ from)
             (pretty-print-typ to)))))

and we modify the unify function in semantic.rkt:

(_ (raise (format "cannot unify type ~a and ~a" (pretty-print-typ t1) (pretty-print-typ t2))))

For example: (typ:arrow (typ:constructor "int" '()) (typ:constructor "int" '())) would be int -> int, very good.

Macro for module language

Then we start handling macros in Racket, to handle the whole module, we need to overwrite #%module-begin(modify main.rkt):

#lang racket

(require (for-syntax syntax/parse)
         racket/syntax
         syntax/stx)
(require "lang.rkt"
         "semantic.rkt"
         "pretty-print.rkt")

(provide (except-out (all-from-out racket) #%module-begin)
         (rename-out [module-begin #%module-begin]))

(define-syntax-rule (module-begin EXPR ...)
  (#%module-begin
   (define all-form (list (parse EXPR) ...))
   (for-each (λ (form)
               (displayln form)
               (printf "type:- ~a~n" (pretty-print-typ (type/infer form))))
             all-form)))

We haven't defined parse, here shows how to get all forms in the module and handling them by for-each, then is parse part:

(define-syntax (parse stx)
  (define-syntax-class bind
    (pattern (bind-name:id bind-expr)
             #:with bind
             #'(cons (symbol->string 'bind-name) (parse bind-expr))))
  (syntax-parse stx
    (`[(~literal let) (binding*:bind ...) body]
     #'(expr:let (list binding*.bind ...) (parse body)))
    (`[(~literal λ) (ps* ...) body] #'(expr:lambda (list (symbol->string 'ps*) ...) (parse body)))
    (`[(~literal quote) (elem* ...)] #'(expr:list (list (parse elem*) ...)))
    (`[f arg* ...] #'(expr:application (parse f) (list (parse arg*) ...)))
    (`v:id #'(expr:variable (symbol->string 'v)))
    (`s:string #'(expr:string (#%datum . s)))
    (`b:boolean #'(expr:bool (#%datum . b)))
    (`i:exact-integer #'(expr:int (#%datum . i)))))
;;; module-begin

Just mapping S expression to expression defined in lang.rkt.

Module reader

Define a module reader:

(module reader syntax/module-reader
  hindley-milner)

With these, you can use #lang hindley-milner as new Racket program:

#lang hindley-milner

(let ([a 1]
      [b (λ (x) x)])
  (b a))

Run it can see program prints expressions' structure and type.

REPL

The final thing to do, that's REPL supporting, we need to overwrite #%top-interaction to make it:

(provide (except-out (all-from-out racket) #%module-begin #%top-interaction)
         (rename-out [module-begin #%module-begin]
                     [top-interaction #%top-interaction]))

(define-syntax-rule (top-interaction . exp)
  (pretty-print-typ (type/infer (parse exp))))

It gives a type after pretty print for input in REPL. Finally, we complete this journey.

Conclusion

I hope detailed implementation and examples show why we need the HM system, and how to make one, and where we would need it. I would be glad to hear you get help from this article. Have a nice day, and it's time for cookies!

p.s. This is probably the second-longest article I made XD.

De Bruijn index: why and how

林子篆 — Sat, 16 May 2020 00:00:00 +0000

At the beginning of learning PLT, everyone would likely be confused by some program that didn't have a variable! Will, I mean they didn't use String, Text or something like that to define a variable. A direct mapping definition of lambda calculus(we would use LC as the short name in the following context, and if you unfamiliar with LC , you can read this article first) usually looks like this:

#lang typed/racket

(struct term [] #:transparent)
(struct term:var term [(name : String)] #:transparent)
(struct term:lambda term [(x : String) (m : term)] #:transparent)
(struct term:application term [(t1 : term) (t2 : term)] #:transparent)

But what we may find some definitions look like this:

#lang typed/racket

(struct bterm [] #:transparent)
(struct bterm:var bterm [(v : Integer)] #:transparent)
(struct bterm:lambda bterm [(m : bterm)] #:transparent)
(struct bterm:application bterm [(t1 : bterm) (t2 : bterm)] #:transparent)

There has two significant different:

variable is an Integer.
lambda does not contain x(which means parameter in high-level languages' concept).

This is De Bruijn index(we would use DBI as short name in the following context), we can write it out, for example, id function λx.x can be rewritten with λ0, Y combinator λf.(λx.f (x x)) (λx.f (x x)) can be rewritten with λ(λ0 (1 1))(λ0 (1 1)), but why? To understand DBI , we need to know what was the problem in LC.

α\alphaα-conversion

Usually, two id functions considered the same function. However, if we encode LC as the first definition written in racket , we would get into trouble: We may say λx.x is not the same function as λy.y, when they are the same. To solve this problem, we developed a conversion called α\alphaα-conversion (or α\alphaα-renaming ), which renaming λx.x and λy.y to λa.a(a is an abstraction variable, we can use any, any character to replace it) let's say. Looks good, any problem else? Emm...yes, as we know, the real world never make thing easier, but that also means a challenge is coming, and we all love the challenge! When a λy.λx.x be renamed to λa.λa.a is fine, because of every programmer work with variable-shadowing for a long-long time. However, there has a possible dangerous conversion is the renamed variable existed! For example, λx.λa.x should not simply be rewritten with λa.λa.a, because later when we rename a, we would get λa.λb.b, oops. λx.λa.x definitely is not λa.λb.b. To correct α\alphaα-conversion is really hard, that's the main reason we introducing the De Bruijn index.

De Bruijn Index

We already seem some examples, but why it resolves the problem we mentioned in the previous section? We need to know those rules used by the conversion process:

remember the level of λ, every time we found a λ when converting recursively, it should increase(or decrease, it depends on index order) this level value.
when found a λ, replace it's x by variable using the De Bruijn index form, the value of the index is the current level.

Let's manually do this conversion:

λx.λy.λz.z
-> λλy.λz.z // x = cur_level = 0, cur_level+1
-> λλλz.z // y = cur_level = 1, cur_level+1
-> λλλ2 // z = cur_level = 2

Notice that since new form of abstraction(a.k.a lambda) only needs M part(a.k.a. body). Another important thing is some De Bruijn index use reverse order than we show at here, so would be λλλ0, not λλλ2.

Implementation

Now, it's time for the program:

(: convert (->* [term] [(Immutable-HashTable String Integer)] bterm))
(define (convert t [rename-to (make-immutable-hash '())])
  (match t
    ;; get index from environment
    ([term:var name] (bterm:var (hash-ref rename-to name)))
    ([term:lambda p b]
     (bterm:lambda
      (convert b
               ;; bind parameter name to an index
               (hash-set rename-to p (hash-count rename-to)))))
    ([term:application t1 t2]
     (bterm:application
      (convert t1 rename-to)
      (convert t2 rename-to)))))

->* is a type constructor in Racket for optional parameters, should be read like (->* normal-parameter-types optional-parameter-types return-type). I use optional parameters to help users don't need to remember they must provide an empty hash table. A tricky thing is I didn't record level, at least, not directly. Here I use an immutable hash table to remember level, since how many variables should be renamed exactly is level value. Then variable only need to replace its name with the index.

Congratulation, now you know everything about DBI!? No, not yet, there still one thing you need to know.

β\betaβ-reduction

β\betaβ-reduction? You might think how can such basic things make things go wrong. However, a naive implementation of β\betaβ-reduction can break structural equivalence of DBI form, which can make an annoying bug in those systems based on LC. The problem is lack-lifting. For example, a normal implementation of β\betaβ-reduction would simply make λ(λλ2 0) become λλ2. However, the same form directly converted from λx.λz.z would become λλ1, and λλ2 will be considered as different value as λλ1 since 1 is not 2. We can introduce another renaming for these, but if we can fix it in β\betaβ-reduction, why need another phase?

Implementation

(: beta-reduction (->* [bterm] [Integer (Immutable-HashTable Integer bterm)] bterm))
(define (beta-reduction t [de-bruijn-level 0] [subst (make-immutable-hash '())])
  (match t
    ([bterm:var i]
     (hash-ref subst i (λ () t)))
    ([bterm:lambda body]
     (bterm:lambda (beta-reduction body (+ 1 de-bruijn-level) subst)))
    ([bterm:application t1 t2]
     (match t1
       ([bterm:lambda body]
        (let ([reduced-term (beta-reduction body (+ 1 de-bruijn-level)
                                            (hash-set subst de-bruijn-level t2))])
          ;;; dbi lifting by replace reduced-term (+ 1 dbi) with (var dbi)
          (beta-reduction reduced-term de-bruijn-level
                          (hash-set subst (+ 1 de-bruijn-level) (bterm:var de-bruijn-level)))))
       (_ (raise "cannot do application on non-lambda term"))))))

We have to record level independently since it has no relation with the substitution map this time. For variables, all need to do is apply substitution map to get value, if not, use origin form as a result. For the lambda, increase level is the only thing. For application, it's complicated. We need to be more careful with it. It contains three major parts:

check t1 is an abstraction(a.k.a lambda), line 9 and 16
do β\betaβ-reduction by add stuff into substitution map, line 11 to 12
DBI lifting (for example, λλ2 should become λλ1), line 14 to 15

Conclusion

DBI is a quite useful technology when implementing complicated AST conversion. It's not just easier to avoid rename conflicting, but also a less memory required form for implementations. I hope you enjoy the article and have a nice day if this even really helps you in a real task, would be awesome!

How to parse expression with the parser combinator

林子篆 — Sun, 03 May 2020 00:00:00 +0000

WARN: As usual, I don't want to fix LaTeX stuff in the article.

Writing parser is a boring and massive job, therefore, people create many ways like parser generators to reduce costs. One of them called parser combinator, parser combinator solves two problems: 1. didn't massive as the hand-crafted parser, 2. didn't impossible to debug like parser generator. Well, it sounds perfect, doesn't it? A parser combinator is great, but one thing could be a problem: precedence descent parser. Unlike parser generator usually provided builtin supporting for operators' precedence. Parser combinator usually only provided basic support for sequence and selective parsing. You probably already heard about operator precedence parser, let's first take a look at its pseudo code(provided by Wiki):

parse_expression()
    return parse_expression_1(parse_primary(), 0)
parse_expression_1(lhs, min_precedence)
    lookahead := peek next token
    while lookahead is a binary operator whose precedence is >= min_precedence
        op := lookahead
        advance to next token
        rhs := parse_primary ()
        lookahead := peek next token
        while lookahead is a binary operator whose precedence is greater
                 than op's, or a right-associative operator
                 whose precedence is equal to op's
            rhs := parse_expression_1 (rhs, lookahead's precedence)
            lookahead := peek next token
        lhs := the result of applying op with operands lhs and rhs
    return lhs

Unfortunately, this is not suitable to port on to a parser based on combinator, because figure out how to introduce state monad into parser monad is a complex job, but that would not be a problem since we have a more intuitive solution which starts from avoiding the left recursion. If you have ever taken a compiler class and it, unfortunately, spend most of the time on parsing, then you may be heard left recursion:

A→AαA \rightarrow A \alphaA→Aα

Where α\alphaα is any sequence of terminal and non-terminal symbols. For example:

Expression→Expression+TermExpression \rightarrow Expression + TermExpression→Expression+Term

A naive implementation would loop on expression() forever. For example:

#lang racket

(define (expression)
  (expression)
  ; in Racket, a char `k` express as `#\k`
  (match #\+)
  (term))

To solve this problem, first, we break down syntax:

Factor→IntegerMultipleExpr→Factor ∗ FactorAdditionExpr→MultipleExpr + MultipleExprFactor \rightarrow Integer \
MultipleExpr \rightarrow Factor \; * \; Factor \
AdditionExpr \rightarrow MultipleExpr \; + \; MultipleExprFactor→IntegerMultipleExpr→Factor∗FactorAdditionExpr→MultipleExpr+MultipleExpr

Then we map them to parser combinators:

#lang racket

(require data/monad data/applicative)
(require megaparsack megaparsack/text)

(define lexeme/p
  ;;; lexeme would take at least one space or do nothing
  (do (or/p (many+/p space/p) void/p)
    (pure (λ () 'lexeme))))

(define (op/p op-list)
  (or/p (one-of/p op-list)
        void/p))
(define factor/p
  (do [expr <- integer/p]
    (lexeme/p)
    (pure expr)))
(define (binary/p high-level/p op-list)
  (do [e <- high-level/p]
    ; `es` parse operator then high-level unit, for example, `* 1`.
    ; therefore, this parser would stop when the operator is not expected(aka. operator is in op-list)
    ; rely on this fact we can leave this loop
    [es <- (many/p (do [op <- (op/p op-list)]
                     (lexeme/p)
                     [e <- high-level/p]
                     (pure (list op e))))]
    (pure (foldl
           (λ (op+rhs lhs)
             (match op+rhs
               [(list op rhs)
                (list op lhs rhs)]))
           e es))))
(define mul:div/p
  (binary/p factor/p '(#\* #\/)))
(define add:sub/p
  (binary/p mul:div/p '(#\+ #\-)))
(define expr/p add:sub/p)

Let's check its result: (parse-string expr/p "1 + 2 * 3 / 4 - 5") generate: (success '(#\- (#\+ 1 (#\/ (#\* 2 3) 4)) 5)) just as expected. Seems like expr/p is our target, but it still is a little massive, doesn't it? We have to modify the definition of each small parser once we need to insert more infix operators. To avoid this, finally going to the purpose of this article, we need an automatic way to do this for us. Observing the definition of parsers, there has a pattern: every infix operator layer can be a (binary/p high-level/p op-list). Using this fact we can create a recursive function:

(define (table/p base/p list-of-op-list)
  (if (empty? list-of-op-list)
      base/p
      (table/p (binary/p base/p (car list-of-op-list))
               (cdr list-of-op-list))))
(define expr/p
  (table/p factor/p
           '((#\* #\/)
             (#\+ #\-))))

The function takes a high-level parser and rest list of operator list. Use the head(car in Racket) of the list of operator list to create a layer parser via binary/p. If the list of operator list hasn't been empty, create more layers via table/p. Now we can handle infinite infix operators! Now, is time to take a break and have fun, have a nice day!

Explain Homotopy type theory like I'm five

林子篆 — Tue, 14 Apr 2020 06:06:16 +0000

As the title, I'm looking for a clear overview summary of HOTT.

From Functor to Applicative

林子篆 — Sat, 11 Apr 2020 13:54:18 +0000

Last time we introduce Functor, a Functor is a container which provide a function can help another function operating the Functor. This function has a name fmap in Haskell. Therefore, a function take a type a as parameter(a -> b) can be lifted by fmap to handle M a, if M provided a fmap. For example, Maybe is a Functor, (+1) has the type Int -> Int, fmap (+1) (Just 10) get a result: Just 11.

Limitation of Functor

Oh, Functor seems so powerful, but programming is simple, life is hard! In the real world, a common situation is there has many M have to handle. For example:

replicateMaybe :: Maybe Int -> Maybe a -> Maybe [a]
replicateMaybe (Just len) (Just a) = Just $ replicate n a
replicateMaybe _ Nothing = Nothing
replicateMaybe Nothing _ = Nothing

Can see that we fall back to pattern matching, line 3 and 4 exclude no input. We can make it easier by extract out this pattern:

liftMaybe2 :: (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
liftMaybe2 f (Just a) (Just b) = Just $ f a b
liftMaybe2 _ _ _ = Nothing

Now liftMaybe2 repliacte a b can work just as expected. Sounds great? How about lift a -> b -> c -> d to M a -> M b -> M c -> M d. How about make a lift to another M, e.g. List? liftList? It seems like boilerplate code, right?

Now we have two problems:

liftMaybe_n problem, how to handle liftMaybe for all n.
liftM problem, how to handle lift for different M.

Indeed, let's dig into fmap again. Every function with type a -> b become M a -> M b, therefore, a -> b -> c would be M a -> M (b -> c). The key point is how to make M (b -> c) applied b.

applyMaybe :: Maybe (a -> b) -> Maybe a -> Maybe b
applyMaybe (Just f) (Just a) = Just $ f a
applyMaybe _ _ = Nothing

Now take a look at how magic happened:

sum :: Int -> Int -> Int -> Int
sum a b c = a + b + c

(fmap sum $ Just 1) `applyMaybe` Just 2 `applyMaybe` Just 3
-- Just 6

We solve liftMaybe_n problem! The only problem is it only works for Maybe, to solve the problem, it's the time of class.

Applicative can help!

class Functor f => Applicative f where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b

<*> is the general version of applyMaybe. pure could raise a variable into the calculation in Applicative, we also call this minimum context.

Special helper `<$>`

<$> has definition as below:

(<$>) :: Functor f => (a -> b) -> f a -> f b
(<$>) = fmap

It just an alias of fmap to help infix syntax:

(+) <$> Just 1 <*> Just 2
-- Just 3
replicate <$> Just 3 <*> Just 'x'
-- Just "xxx"
replicate <$> [1, 2, 3] <*> ['x', 'y', 'z']
-- ["x", "y", "z", "xx", "yy", "zz", "xxx", "yyy", "zzz"]

Conclusion

I hope this article really help you understand why we need Applicative. Next time would Monad or monoid, thanks for your read and have a good day!

Binary Encoding of Integer

林子篆 — Sat, 21 Mar 2020 00:00:00 +0000

Warning: I don't want to fix those LaTeX formulae anymore, go to https://dannypsnl.github.io/docs/cs/binary-encoding-of-interger/ if you want to see them.

\mathbb{Z} contains positive and negative numbers, but nowdays Computer system based on binary. There only have 0 and 1 can be used. A simple solution is: put signed symbol at the most significant bit. For example, use 8 bits can represent:

-(2^7 - 1) = -127, -126, -125, … -0, +0, …, +125, +126, +(2^7 - 1) = +127

This is an intuitive way. Therefore, early days computers applied it.

But this way(called Sign magnitude ) has two big problems:

waste a place: +0 and -0 are different in this system
have to detect signed or not and use different ways to do an operation like addition

One’s complement

To solve the second problem with the calculation complex, engineers introduce one’s complement. For example, a number: -43_{10} is 100101011_2, the one’s complement of it is 111010100_2(keep the most significant bit and reverse the rest of bits). It still only works for -127_{10} ... 127_{10} with 8 bits, didn’t solve the first problem obviously, why we say it solves the second one? Because we can replace special digital electronics with two subtractions:

0010 - 0001 \equiv 0010 + (0011 - 0001) + (0001 - 0100)

Then we convert negative number to one’s complement, and remember end-around carry(the bit over most significant bit should be add back), then get:

0010 + 0011 + 1110 + 0001 + 1011
\
\to 0101 + 1110 + 0001 + 1011
\
\to 10011 + 0001 + 1011
\
\to 10100 + 1011
\
\to 1[1111]
\
\to 1111 + 0001
\
\to 1[0000]
\
\to 0000 + 0001
\
\equiv 0001

Or 1110 + 0010 would get 1[0000] \to 0001

Benefit

no need to check signed bit
reverse bits can use addition on subtraction

Problem

need a special unit for end-around carry
there still have two zero representations

Two’s complement

Modular Arithmetic

If we have an integer use 3 bits to represent, then 7 + 1 \equiv 0(mod \; 8) because of the overflow.

If we have k bits for an integer, then we can generalize to A + B \equiv C(mod \; 2^k).

Abelian group

For additive, we have to implement an Abelian group: an Identity element and every element has an Inverse element that adds them would get the Identity element.

Now consider how can our 3-bits integer fit rules of Abelian group? If [000] represents 0, it’s identity in our group. Assuming [001] is 1, how to know the representation of -1? It’s easy to get [111] this answer because we know [111] + [001] = 1[000], overflow would be dropped. And it cannot be any number except -1, else we cannot find others inverse element of 1. With this, we can keep finding an inverse for 2([010]) is [110] and so on.

On the other hand, it still simple: -1 is the biggest negative number in 3-bits encoding. Follows unsigned order, [111] > [110], then don’t need another way to compare numbers.

Properties

Now we can see we map all possible combinations of bits to an exact number. Solve the first problem in previous solutions.

Even more, the subtractive of signed integer is additive of unsigned number: 010 + 101 can be 2 + 5 or 2 + (-3). Therefore:

A + \neg A = 2^k - 1
\
\to A + (\neg A + 1) = 2^k(mod \; 2^k)
\
\to -A := \neg A + 1

Now we know we don’t need subtractive, it can be replaced with one’s complement plus one.

Back to group, one’s complement would waste place about encoding is a thing must happen, because in 3-bits encoding it maps [111] and [000]. In two’s complement the axis of symmetry pass through [000], therefore, we won’t get repetitive representations of zero.

Extend this [001] maps to [111] in two’s complement, maps to [110] in one’s complement. Therefore, one’s complement plus one would be two’s complement.

NOTE: simply typed lambda calculus

林子篆 — Sun, 08 Mar 2020 00:00:00 +0000

Last time I introduce lambda calculus.Lambda calculus is powerful enough for computation. But it’s not good enough for people, compare with below Church Numerals

\lambda m. \lambda n. \lambda s. \lambda z. m\;s\;(n\;s\;z)

people prefer just + more.

But once we introduce such fundamental operations into the system, validation would be a thing. This is the main reason to have a λ→ system(a.k.a. simply typed lambda calculus). It gets name λ→ is because it introduces one new type: Arrow type, represent as T1→T2 for any abstraction λx.M where x has a type is T1 and M has a type is T2. Therefore we can limit the input to a specified type, without considering how to add two Car together!

To represent this, syntax needs a little change:

term ::= terms
  x variable
  λx: T.term abstraction
  term term application

Abstraction now can describe it’s parameter type. Then we have typing rules:

\frac{ x:T \in \Gamma }{ \Gamma \vdash x:T } \;\;\;\; T-Variable

\frac{ \Gamma, x:T_1 \vdash t_2: T_2 }{ \Gamma \vdash \lambda x:T_1.t_2 : T_1 \to T_2 } \;\;\;\; T-Abstraction

\frac{ \Gamma, t_1:T_1 \to T_2 \; \Gamma \vdash t_2: T_1 }{ \Gamma \vdash t_1 \; t_2 : T_2 } \;\;\;\; T-Application

Here is the explanation:

T-Variable: with the premise, term x binds to type T in context Γ is truth. We can make a conclusion, in context Γ, we can judge the type of x is T.
T-Abstraction: with the premise, with context Γ and term x binds to type T1 we can judge term t2 has type T2. We can make a conclusion, in context Γ, we can judge the type of λx:T1.t2 is T1→T2.
T-Application: with the premise, with context Γ and term t1 binds to type T1→T2 and with context Γ we can judge term t2 has type T1. We can make a conclusion, in context Γ, we can judge the type of t1t2 is T2.

A Racket macro tutorial – get HTTP parameters easier

林子篆 — Sun, 16 Feb 2020 00:00:00 +0000

A few days ago, I post this answer to respond to a question about Racket's web framework. When researching on which frameworks could be used. I found no frameworks make get values from HTTP request easier. So I start to design a macro, which based on routy and an assuming function http-form/get, as following shows:

(get "/user/:name"
  (lambda ((name route) (age form))
    (format "Hello, ~a. Your age is ~a." name age)))

Let me explain this stuff. get is a macro name, it's going to take a string as route and a "lambda" as a request handler. ((name route) (age form)) means there has a parameter name is taken from route and a parameter age is taken from form. And (format "Hello, ~a. Your age is ~a." name age) is the body of the handler function.

Everything looks good! But we have no idea how to make it, not yet ;). So I'm going to show you how to build up this macro step by step, as a tutorial.

First, we have to ensure the target. I don't want to work with original Racket HTTP lib because I never try it, so I pick routy as a routing solution. A routy equivalent solution would look like:

(routy/get "/user/:name"
  (lambda (req params)
    (format "Hello, ~a. Your age is ~a." (request/param params 'name) (http-form/get req "age"))))

WARNING: There has no function named http-form/get, but let's assume we have such program to focus on the topic of the article: macro

Now we can notice that there was no name, age in lambda now. But have to get it by using request/param and http-form/get. But there also has the same pattern, the route! To build up macro, we need the following code at the top of the file macro.rkt first:

#lang racket

(require (for-syntax racket/base racket/syntax syntax/parse))

Then we get our first macro definition:

(define-syntax (get stx)
  (syntax-parse stx
    [(get route:str)
      #'(quote
        (routy/get route
          (lambda (req params)
            'body)))]))

(get "/user/:name")
; output: '(routy/get "/user/:name" (lambda (req params) 'body))

Let's take a look at each line, first, we have define-syntax, which is like define but define a macro. It contains two parts, name and syntax-parse. The name part was (get stx), so the macro called get, with a syntax object stx. The syntax-parse part was:

(syntax-parse stx
  [(get route:str)
    #'(quote
      (routy/get route
        (lambda (req params)
          'body)))])

The syntax-parse part works on the syntax object, so it's arguments are a syntax object and patterns! Yes, patterns! It's ok to have multiple patterns like this:

(define-syntax (multiple-patterns? stx)
  (syntax-parse stx
    [(multiple-patterns? s:str) #'(quote ok-str)]
    [(multiple-patterns? s:id) #'(quote ok-id)]))

(multiple-patterns? "")
; output: 'ok-str
(multiple-patterns? a)
; output: 'ok-id

Now we want to add handler into get, to reduce the complexity, we introduce another feature: define-syntax-class. The code would become:

(define-syntax (get stx)
  (define-syntax-class handler-lambda
    #:literals (lambda)
    (pattern (lambda (arg*:id ...) clause ...)
      #:with
      application
      #'((lambda (arg* ...)
           clause ...)
         arg* ...)))

  (syntax-parse stx
    [(get route:str handler:handler-lambda)
      #'(quote
        (routy/get route
          (lambda (req params)
            handler.application)))]))

First we compare syntax-parse block, we add handler:handler-lambda and handler.application here:

(syntax-parse stx
  [(get route:str handler:handler-lambda)
    #'(quote
      (routy/get route
        (lambda (req params)
          handler.application)))]))

This is how we use a define-syntax-class in a higher-level syntax. handler:handler-lambda just like route:str, the only differences are their pattern. route:str always expected a string, handler:handler-lambda always expected a handler-lambda. And notice that handler:handler-lambda would be the same as a:handler-lambda, just have to use a to refer to that object. But better give it a related name.

Then dig into define-syntax-class:

(define-syntax-class handler-lambda
  #:literals (lambda)
  (pattern (lambda (arg*:id ...) clause* ...)
    #:with
    application
    #'((lambda (arg* ...)
        clause* ...)
        arg* ...)))

define-syntax-class allows us add some stxclass-option, for example: #:literals (lambda) marked lambda is not a pattern variable, but a literal pattern. The body of define-syntax-class is a pattern, which takes a pattern and some pattern-directive. The most important pattern-directive was #:with, which stores how to transform this pattern, it takes a syntax-pattern and an expr, as you already saw, this is usage: handler.application.

The interesting part was ... in the pattern, it means zero to many patterns. A little tip makes such variables with a suffix * like arg* and clause* at here.

Now take a look at usage:

(get "/user/:name"
  (lambda (name age)
    (format "Hello, ~a. Your age is ~a." name age)))
; output: '(routy/get "/user/:name" (lambda (req params) ((lambda (name age) (format "Hello, ~a. Your age is ~a." name age)) name age)))

There are some issues leave now, since we have to distinguish route and form, current pattern of handler-lambda is not enough. The handler-lambda.application also incomplete, we need

(lambda (req params)
  (format "Hello, ~a. Your age is ~a."
          (request/param params 'name)
          (http-form/get req "age")))

but get

(lambda (req params)
  ((lambda (name age)
    (format "Hello, ~a. Your age is ~a."
            name
            age)) name age))

right now.

To decompose the abstraction, we need another define-syntax-class.

(define-syntax-class argument
    (pattern (arg:id (~literal route))
      #:with get-it #'[arg (request/param params 'arg)])
    (pattern (arg:id (~literal form))
      #:with get-it #'[arg (http-form/get req (symbol->string 'arg))]))

(define-syntax-class handler-lambda
  #:literals (lambda)
  (pattern (lambda (arg*:argument ...) clause* ...)
    #:with
    application
    #'(let (arg*.get-it ...)
         clause* ...)))

There are two changes, replace lambda with let in handler-lambda.application(it's more readable), and use argument syntax type instead of id.

argument has two patterns, arg:id (~literal route) and arg:id (~literal form) to match (x route) and (x form). Notice that #:literals (x) and (~literal x) has the same ability, just pick a fit one. symbol->string converts an atom to a string, here is an example:

(symbol->string 'x)
; output: "x"

Let's take a look at usage:

(get "/user/:name"
  (lambda ((name route) (age form))
    (format "Hello, ~a. Your age is ~a." name age)))
; output: '(routy/get "/user/:name" (lambda (req params) (let ((name (request/param params 'name)) (age (http-form/get req (symbol->string 'age)))) (format "Hello, ~a. Your age is ~a." name age))))

Manually pretty output:

'(routy/get "/user/:name"
  (lambda (req params)
    (let ((name (request/param params 'name))
          (age (http-form/get req (symbol->string 'age))))
      (format "Hello, ~a. Your age is ~a." name age))))

Summary

With make up this tutorial, I learn a lot of macro tips in Racket that I don't know before. I hope you also enjoy this, also hope you can use everything you learn from here to create your helpful macro. Have a nice day.

End up, all code

#lang racket

(require (for-syntax racket/base racket/syntax syntax/parse))

(define-syntax (get stx)
  (define-syntax-class argument
    (pattern (arg:id (~literal route))
      #:with get-it #'[arg (request/param params 'arg)])
    (pattern (arg:id (~literal form))
      #:with get-it #'[arg (http-form/get req (symbol->string 'arg))]))

  (define-syntax-class handler-lambda
    #:literals (lambda)
    (pattern (lambda (arg*:argument ...) clause* ...)
      #:with
      application
      #'(let (arg*.get-it ...)
           clause* ...)))

  (syntax-parse stx
    [(get route:str handler:handler-lambda)
      #'(quote
        (routy/get route
          (lambda (req params)
            handler.application)))]))

(get "/user/:name"
  (lambda ((name route) (age form))
    (format "Hello, ~a. Your age is ~a." name age)))

NOTE: bounded polymorphism

林子篆 — Fri, 24 Jan 2020 00:00:00 +0000

Bounded polymorphism refers to existential quantifiers(∃), restricted to range over types of bound type. To understand it only needs a few examples. Let’s start! Take a look at the following program:

numSort :: Num a => [a] -> [a]

Num a is how we represent the bounded polymorphism in Haskell , the definition of Num was class Num b where(Hoogle shows a, just prevent to confuse reader don’t familiar with Haskell ) could read as a type b is an instance of class Num.

So numSort takes [a] only if a is an instance of Num. Now we could run down:

numSort [1, 2, 3] :: [Int]
numSort [1.1, 2, 3] :: [Double]

This is really a powerful feature(and you don’t need to use Haskell for this, Java also has this feature), consider the old way to do List<A> to List<B>, and unfortunately solution was to copy each element in the list.

Type as Constraint: Why we need more type?

林子篆 — Thu, 16 Jan 2020 00:00:00 +0000

For me, programming was about how to map my mind to the world; from this view, it probably shows why I tend to use statically typed language. A strong model could ensure more people won't misunderstand our purpose. This article was going to show some strategy to promise the thing works in our mind won't be broken by others accident.

Now consider a situation, we had a list of something and we just sort it and we want to do binary-search with it. A subtle problem was we were hard to ensure the list was sorted. In the language such as Python or C, we had to promise this by ourselves. So we insert assert(sorted(list)) into our program like this:

def binary_search(lst):
    assert sorted(lst)
    # ...

p.s. More assertion in Python, I'm not a Python master. I have to say.

And then we feel the program became slower. Because we were so smart, we distinguish debug and release environment, there were no assertions in release mode. Now everything runs good, right? Well, if you wrote some programs with verified data, that's ok. But what if the lst came from the user input? It probably would break, or let's be honest, it would break. So remove checking from there shouldn't happen. But many languages cannot ensure it, we have to take responsibility.

With wrapping, we can make it a little bit better. We can do this:

func Sort(lst []interface{}) SortedList {
    // sorting
    return SortedList{lst: lst}
}

type SortedList struct {
    lst []interface{}
}

func BinarySearch(lst SortedList) interface{} {
    // you know, just ignore how we get the element
    return element
}

func main() {
    lst := []interface{}{1}
    sortedLst := Sort(lst)
    _ = BinarySearch(sortedLst)
}

But this is a weak promise, anyone can just use SortedList{lst: lst} to break it, but better than no promise. But already easier to find out in code review.

The problem was this is not just easy to break, but it also didn't promise enough information for us. What if we modify the list before we use BinarySearch? This promise required some human work to check it. Now we want a more improved version. A promise that cannot be violated and doesn't need human work to check the mechanism. As usual, I would use pseudo-code(to get more information, ref to my another article):

sort[T: comparable](list: List[T]): Output
where
  Output = List[T] // type alias
  Output <: sorted // now we know the result type was a subtype of `sorted`
{
  // sorting
}

binary_search[T: comparable](list: List[T] <: sorted): T {
  // do something and get the answer
  return element;
}

and then we can use them like:

sorted_list: List[int] = sort(list);
_: int = binary_search(sorted_list); // `_` explicitly ignore value

The most important thing is when we do operations that do not fit trait sorted the program work as usual but the compiler won't think the value was sorted anymore, e.g.

sorted_list: List[int] = sort(list);
sorted_list.push(3); // add element
_: int = binary_search(sorted_list);

Now it won't get compiled, because the type mismatching, we can do push on List[int], but after that sorted_list won't belong to sorted trait anymore. Do you probably think why not make another type? Because although we, of course, can do that, it would be bad modeling in another case, when we just sort a list and later keep doing something on it and don't care about it's sorted or not til next sort, create another type would let we must keep converting type manually, which violate our spirit! Now back, sorted trait modeled the situation very well, we only have to give tag, the compiler checks the rest. We still have checking, we have to ensure the part need to do binary_search get List[T] <: sorted, but this is better than adding assertion everywhere. I hope you have a nice day and thanks for the read.

Forem: 林子篆

A wrong question: Is a Square a Rectangle?

What is Subtyping?

What is Liskov Substitution Principle(LSP)?

What's the problem

Solution

How to find mk fixed point

Hindley-Milner type system: Incrementally build way & Make new language in Racket

Why?

Why Polymorphism

Setup a project

Syntax Overview

Part I: Incrementally build up inference

Monomorphism stuff

List

Variable

Lambda

Bind variable

Infer

Let polymorphism

Application

Unify freevar

Occurs check

Part Two: Make new language in Racket

Pretty Print

Macro for module language

Module reader

REPL

Conclusion

De Bruijn index: why and how

α\alphaα-conversion

De Bruijn Index

Implementation

β\betaβ-reduction

Implementation

Conclusion

How to parse expression with the parser combinator

Explain Homotopy type theory like I'm five

From Functor to Applicative

Limitation of Functor

Applicative can help!

Special helper <$>

Conclusion

Binary Encoding of Integer

One’s complement

Benefit

Problem

Two’s complement

Modular Arithmetic

Abelian group

Properties

NOTE: simply typed lambda calculus

A Racket macro tutorial – get HTTP parameters easier

Summary

End up, all code

NOTE: bounded polymorphism

Type as Constraint: Why we need more type?

Special helper `<$>`