VVbuys Blog

1
2
3
4
5
6

Z ::= X;;
Y ::= 1;;
WHILE ~(Z = 0) DO
  Y ::= Y * Z;;
  Z ::= Z - 1
END

A weird convention through out all IMP is:

• a-: arith
• b-: bool
• c-: command

Arithmetic and Boolean Expression

Abstract Syntax

1
2
3
4
5
6
7
8
9
10
11
12

a ::=
    | nat
    | a + a
    | a - a
    | a * a
b ::= 
    | true
    | false
    | a = a
    | a ≤ a
    | ¬b
    | b && b

1
2
3
4
5
6
7
8
9
10
11
12

Inductive aexp : Type :=
  | ANum (n : nat)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).
Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Evaluation

TODO: is this considered as “denotational semantics”?

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n ⇒ n
  | APlus a1 a2 ⇒ (aeval a1) + (aeval a2)
  | AMinus a1 a2 ⇒ (aeval a1) - (aeval a2)
  | AMult a1 a2 ⇒ (aeval a1) * (aeval a2)
  end.
Fixpoint beval (b : bexp) : bool :=
  match b with
  | BTrue ⇒ true
  | BFalse ⇒ false
  | BEq a1 a2 ⇒ (aeval a1) =? (aeval a2)
  | BLe a1 a2 ⇒ (aeval a1) <=? (aeval a2)
  | BNot b1 ⇒ negb (beval b1)
  | BAnd b1 b2 ⇒ andb (beval b1) (beval b2)
  end.

Supposed we have a Fixpoint optimize_0plus (a:aexp) : aexp

1
2

Theorem optimize_0plus_sound: ∀a,
  aeval (optimize_0plus a) = aeval a.

During the proof, many cases of destruct aexp are similar!
Recursive cases such as APlus, AMinus, AMult all require duplicated IH application.

From Coq Intensive:
when we simpl on APlus case. it’s not “simplified” but give us a pattern matching.
That’s a hint that we need to furthur case analysis by destruct n as 0 case or _ case.

Coq Automation

Tacticals

“higher-order tactics”.

try T and ; tacticals

if T fail, try T successfully does nothing at all

T;T' : performs T' on each subgoal generated by T.

Super blindly but useful: (only leave the “interesting” one.)

1
2
3
4
5

induction a;
    (* Most cases follow directly by the IH... *)
    try (simpl; rewrite IHa1; rewrite IHa2; reflexivity).
    (* ... or are immediate by definition *)
    try reflexivity.

. is the atomic
; cannot be stepped into…

T; [T1 | T2 | ... | Tn] tacticals

general form or ;
T;T' is shorthand for: T; [T' | T' | ... | T'].

repeat tacticals

1
2
3

Theorem In10 : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat (try (left; reflexivity); right). Qed.

• stop when it fails
• always succeeds, then loop forever! e.g. repeat simpl

This does not affect Coq’s logical consistency,
construction process diverges means we have failed to construct a proof, not that we have constructed a wrong one.

Defining New Tactic Notations

• Tactic Notation: syntax extension for tactics (good for simple macros)

1
2

Tactic Notation "simpl_and_try" tactic(c) :=
  simpl; try c.

• Ltac: scripting language for tactics (good for more sophisticated proof engineering)
• OCaml tactic scripting API (for wizards)

The omega Tactic

Presburger arithmetic

• arith, equality, ordering, logic connectives
• O(doubly expontential)

A Few More Handy Tactics

• clear H
• subst x, subst
• rename ... into ... (change auto-generated name that we don’t like…)

the below three are very useful in Coq Automation (w/ try T; T')

• assumption
• contradiction
• constructor (try to apply all constructors.
  Problem: might have multiple constructors applicable but some fail)

Evaluation as a Relation

Defined as Binary relation on aexp × nat.
Exactly Big Step / Structural Operational Semantics.

More flexible than Fixpoint (computation, or Denotational).
…Since we can operate on Inductive as data I guess?
…and we can also induction on the relation.
…and when things getting more and more “un-computable” (see below).

译注：求值关系不满足对称性，因为它是有方向的。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

Inductive aevalR : aexp → nat → Prop :=
  | E_ANum n :
      aevalR (ANum n) n
  | E_APlus (e1 e2: aexp) (n1 n2: nat) :
      aevalR e1 n1 →
      aevalR e2 n2 →
      aevalR (APlus e1 e2) (n1 + n2)
  | E_AMinus (e1 e2: aexp) (n1 n2: nat) :
      aevalR e1 n1 →
      aevalR e2 n2 →
      aevalR (AMinus e1 e2) (n1 - n2)
  | E_AMult (e1 e2: aexp) (n1 n2: nat) :
      aevalR e1 n1 →
      aevalR e2 n2 →
      aevalR (AMult e1 e2) (n1 * n2).

Noticed now we now define inductive in a mixed style:
some arg is before : (named), some are after : (anonymous).

We could do this as well

1
2
3
4

| E_APlus (e1 e2: aexp) (n1 n2: nat)
     (H1 : aevalR e1 n1)
     (H2 : aevalR e2 n2) :
     aevalR (APlus e1 e2) (n1 + n2)

Reserved Notation allow us using the notation during the definition!

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

Reserved Notation "e '\\' n" (at level 90, left associativity).

Inductive aevalR : aexp → nat → Prop :=
  | E_ANum (n : nat) :
      (ANum n) \\ n
  | E_APlus (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 \\ n1) → 
      (e2 \\ n2) → 
      (APlus e1 e2) \\ (n1 + n2)
  | E_AMinus (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 \\ n1) → 
      (e2 \\ n2) → 
      (AMinus e1 e2) \\ (n1 - n2)
  | E_AMult (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 \\ n1) → 
      (e2 \\ n2) → 
      (AMult e1 e2) \\ (n1 * n2)

  where "e '\\' n" := (aevalR e n) : type_scope.

I hated this infix \\ notation…it tries to mimic ⇓ (double down arrow).

                           e1 \\ n1
                           e2 \\ n2
                     -------------------- (E_APlus)
                     APlus e1 e2 \\ n1+n2

is actually:

                           e1 ⇓ n1
                           e2 ⇓ n2
                     -------------------- (E_APlus)
                     APlus e1 e2 ⇓ n1+n2

Coq Intensive:
If you have two variables above the line. Think about if you need generalize dependent.

Computational vs. Relational Definitions INTERESTING

In some cases, relational definition are much better than computational (a.k.a. functional).

for situations, where thing beingdefined is not easy to express as a function (or not a function at all)

case 1 - safe division

1
2

Inductive aexp : Type :=
| ADiv (a1 a2 : aexp). (* <--- NEW *)

• functional: how to return ADiv (ANum 5) (ANum 0)? probably has to be option (Coq is total!)
• relational: (a1 \\ n1) → (a2 \\ n2) → (n2 > 0) → (mult n2 n3 = n1) → (ADiv a1 a2) \\ n3.
  • we can add a constraint (n2 > 0).

case 2 - non-determinism

1
2

Inductive aexp : Type :=
| AAny (* <--- NEW *)

• functional: not a deterministic function…
• relational: E_Any (n : nat) : AAny \\ n … just say it’s the case.

Nonetheless, functional definition is good at:

1. by definition deterministic (need proof in relational case)
2. take advantage of Coq’s computation engine.
3. function can be directly “extracted” from Gallina to OCaml/Haskell

In large Coq developments:

1. given both styles
2. a lemma stating they coincise (等价)

Expressions with Variables

State (Environment) 环境

A machine state (or just state) represents the current values of all variables at some point in the execution of a program.

1

Definition state := total_map nat.

Syntax

1
2

Inductive aexp : Type :=
  | AId (x : string) (* <--- NEW *)

Notations & Coercisons – “meta-programming” and AST quasi-quotation

Quasi-quotation

OCaml PPX & AST quasi-quotation

quasi-quotation enables one to introduce symbols that stand for a linguistic expression in a given instance and are used as that linguistic expression in a different instance.

e.g. in above OCaml example, you wrote %expr 2 + 2 and you get [%expr [%e 2] + [%e 2]].

Coq’s Notation Scope + Coercision == built-in Quasi-quotation

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

(** Coercision for constructors **)
Coercion AId : string >-> aexp.
Coercion ANum : nat >-> aexp.

(** Coercision for functions **)
Definition bool_to_bexp (b : bool) : bexp := if b then BTrue else BFalse.
Coercion bool_to_bexp : bool >-> bexp.

(** Scoped Notation **)
Bind Scope imp_scope with aexp.
Bind Scope imp_scope with bexp.

(** the Extension Point token **)
Delimit Scope imp_scope with imp.

(** now we can write... **)
Definition example_aexp := (3 + (X * 2))%imp : aexp.
Definition example_aexp : aexp := (3 + (X * 2))%imp. 
Definition example_aexp := (3 + (X * 2))%imp.    (* can be inferred *)

Evaluation w/ State (Environment)

Noticed that the st has to be threaded all the way…

1
2
3
4
5
6
7
8

Fixpoint aeval (st : state) (a : aexp) : nat :=
  match a with
  | AId x ⇒ st x (* <--- NEW *)              (** lookup the environment **)
  ...

Fixpoint beval (st : state) (b : bexp) : bool := ...

Compute (aeval (X !-> 5) (3 + (X * 2))%imp). (** ===> 13 : nat **)

Commands (Statement)

1

c ::= SKIP | x ::= a | c ;; c | TEST b THEN c ELSE c FI | WHILE b DO c END

we use TEST to avoid conflicting with the if and IF notations from the standard library.

1
2
3
4
5
6

Inductive com : Type :=
  | CSkip
  | CAss (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

notation magics:

1
2
3
4
5
6

Bind Scope imp_scope with com.
Notation "'SKIP'" := CSkip : imp_scope.
Notation "x '::=' a" := (CAss x a) (at level 60) : imp_scope.
Notation "c1 ;; c2" := (CSeq c1 c2) (at level 80, right associativity) : imp_scope.
Notation "'WHILE' b 'DO' c 'END'" := (CWhile b c) (at level 80, right associativity) : imp_scope.
Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" := (CIf c1 c2 c3) (at level 80, right associativity) : imp_scope.

Unset Notations

1
2
3

Unset Printing Notations.  (** e1 + e2 -> APlus e1 e2 **)
Set Printing Coercions.    (** n -> (ANum n) **)
Set Printing All.

The Locate command

1
2
3
4
5
6

Locate "&&".

(** give you two, [Print "&&"] only give you the default one **)
Notation
"x && y" := andb x y : bool_scope (default interpretation)
"x && y" := BAnd x y : imp_scope

Evaluating Commands

Noticed that to use quasi-quotation in pattern matching, we need

1
2
3
4
5
6

Open Scope imp_scope.
...
  | x ::= a1 =>     (**  CAss x a1  **)
  | c1 ;; c2 =>     (**  CSeq c1 c1 **)
...
Close Scope imp_scope.

An infinite loop (the %imp scope is inferred)

1
2
3
4

Definition loop : com :=
  WHILE true DO
    SKIP
  END.

The fact that WHILE loops don’t necessarily terminate makes defining an evaluation function tricky…

Evaluation as function (FAIL)

In OCaml/Haskell, we simply recurse, but In Coq

1
2
3
4

| WHILE b DO c END => if (beval st b)
                      then ceval_fun st (c ;; WHILE b DO c END)
                      else st
(** Cannot guess decreasing argument of fix **)

Well, if Coq allowed (potentially) non-terminating, the logic would be inconsistent:

1

Fixpoint loop_false (n : nat) : False := loop_false n.   (** False is proved! **)

Step-Indexed Evaluator (SUCC)

Chapter ImpCEvalFun provide some workarounds to make functional evalution works:

1. step-indexed evaluator, i.e. limit the recursion depth. (think about Depth-Limited Search).
2. return option to tell if it’s a normal or abnormal termination.
3. use LETOPT...IN... to reduce the “optional unwrapping” (basicaly Monadic binding >>=!)

• this approach of let-binding became so popular in ML family.

Evaluation as Relation (SUCC)

Again, we are using some fancy notation st=[c]=>st' to mimic ⇓:
In both PLT and TaPL, we are almost exclusively use Small-Step, but in PLC, Big-Step were used:

                      beval st b1 = true
                       st =[ c1 ]=> st'
            ---------------------------------------  (E_IfTrue)
            st =[ TEST b1 THEN c1 ELSE c2 FI ]=> st'

is really:

                        H; b1 ⇓ true
                        H; c1 ⇓ H'
              ----------------------------------  (E_IfTrue)
              H; TEST b1 THEN c1 ELSE c2 FI ⇓ H'

1
2
3
4
5
6
7
8
9
10
11
12
13

Reserved Notation "st '=[' c ']⇒' st'" (at level 40).
Inductive ceval : com → state → state → Prop :=
...
| E_Seq : ∀c1 c2 st st' st'',
    st =[ c1 ]⇒ st' →
    st' =[ c2 ]⇒ st'' →
    st =[ c1 ;; c2 ]⇒ st''
| E_IfTrue : ∀st st' b c1 c2,
      beval st b = true →
      st =[ c1 ]⇒ st' →
      st =[ TEST b THEN c1 ELSE c2 FI ]⇒ st'
...
  where "st =[ c ]⇒ st'" := (ceval c st st').

By definition evaluation as relation (in Type level),
we need to construct proofs (terms) to define example.

…noticed that in the definition of relaiton ceval, we actually use the computational aevel, beval..
…noticed that we are using explicit ∀ style rather than constructor argument style (for IDK reason). They are the same!

Determinism of Evaluation

Changing from a computational to a relational definition of evaluation is a good move because it frees us from the artificial requirement that evaluation should be a total function
求值不再必须是全函数

But it also raises a question: Is the second definition of evaluation really a partial function?
这个定义真的是偏函数吗？（这里的重点在于 偏函数 要求 right-unique 即 deterministic）

we can prove:

1
2
3
4
5

Theorem ceval_deterministic: ∀c st st1 st2,
     st =[ c ]⇒ st1 →
     st =[ c ]⇒ st2 →
     st1 = st2.
Proof. ...

Reasoning About Imp Programs

Case plus2_spec

1
2
3
4
5
6

Theorem plus2_spec : ∀st n st',
  st X = n →
  st =[ plus2 ]⇒ st' →
  st' X = n + 2.
Proof.
  intros st n st' HX Heval.

this looks much better as inference rules:

    H(x) = n
    H; x := x + 2 ⇓ H'
  --------------------- (plus2_spec)
    H'(x) = n + 2

By inversion on the Big Step eval relation, we can expand one step of ceval
(对 derivation tree 的 expanding 过程其实就是展开我们所需的计算步骤的过程)

  st : string -> nat
  =================================
  (X !-> st X + 2; st) X = st X + 2

In inference rule:

  H : string → nat
  ================================
  (x ↦ H(x) + 2); H)(x) = H(x) + 2

Case no_whiles_terminating

1
2
3
4
5
6
7
8

Theorem no_whilesR_terminating_fail:
   forall c, no_whilesR c -> forall st, exists st', st =[ c ]=> st'.
Proof.
  intros.
  induction H; simpl in *. 
  - admit.
  - admit.
  - (* E_Seq *)

If we intros st before induction c,
the IH would be for particular st and too specific for E_Seq
(It’s actually okay for TEST since both branch derive from the same st)

1
2
3
4

IHno_whilesR1 : exists st' : state, st =[ c1 ]=> st'
IHno_whilesR2 : exists st' : state, st =[ c2 ]=> st'
============================
exists st' : state, st =[ c1;; c2 ]=> st'

So we’d love to

1
2
3
4
5
6

generalize dependent st.
induction H...
- specialize (IHno_whilesR1 st).  destruct IHno_whilesR1 as [st' Hc1].
  specialize (IHno_whilesR2 st'). destruct IHno_whilesR2 as [st'' Hc2].  (* specialize [IH2] with the existential of [IH1] **)
  exists st''.
  apply E_Seq with (st'); assumption.

Additional Exerciese

Stack Compiler

Things that evaluate arithmetic expressions using stack:

• Old HP Calculators
• Forth, Postscript
• Java Virtual Machine

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

infix:
      (2*3)+(3*(4-2))

postfix:
      2 3 * 3 4 2 - * +

stack:
      [ ]           |    2 3 * 3 4 2 - * +
      [2]           |    3 * 3 4 2 - * +
      [3, 2]        |    * 3 4 2 - * +
      [6]           |    3 4 2 - * +
      [3, 6]        |    4 2 - * +
      [4, 3, 6]     |    2 - * +
      [2, 4, 3, 6]  |    - * +
      [2, 3, 6]     |    * +
      [6, 6]        |    +
      [12]          |

Goal: compiler translates aexp into stack machine instructions.

1
2
3
4
5
6

Inductive sinstr : Type :=
| SPush (n : nat)
| SLoad (x : string)   (* load from store (heap) *)
| SPlus
| SMinus
| SMult.

Correct Proof

1
2

Theorem s_compile_correct : forall (st : state) (e : aexp),
  s_execute st [] (s_compile e) = [ aeval st e ].

To prove this, we need a stronger induction hypothesis (i.e. more general), so we state:

1
2

Theorem s_execute_theorem : forall (st : state) (e : aexp) (stack : list nat) (prog : list sinstr),
  s_execute st stack (s_compile e ++ prog) = s_execute st ((aeval st e) :: stack) prog.

and go through!

IMP Break/Continue

1
2
3

Inductive result : Type :=
  | SContinue
  | SBreak.

The idea is that we can add a signal to notify the loop!

Fun to go through!

Slide Q & A

st =[c1;;c2] => st'

• there would be intermediate thing after inversion so… we need determinism to prove this!

  • (It won’t be even true in undetermincy)

• the WHILE one (would diverge)

  • true…how to prove?
  • induction on derivation…!
    • show contradiction for all cases

• to prove ¬(∃st', ...), we intro the existentials and prove the False.

Auto

auto includes try

1. Proof with auto.
2. Set Intro Auto

the parser relies on some “monadic” programming idioms

basically, parser combinator (But 非常麻烦 in Coq)

Lex

1
2
3
4
5
6
7
8
9
10

Inductive chartype := white | alpha | digit | other.

Definition classifyChar (c : ascii) : chartype :=
  if      isWhite c then white
  else if isAlpha c then alpha
  else if isDigit c then digit
  else                   other.
  

Definition token := string.

Syntax

带 error msg 的 option:

1
2
3
4
5
6

Inductive optionE (X:Type) : Type :=
  | SomeE (x : X)
  | NoneE (s : string).       (** w/ error msg **)

Arguments SomeE {X}.
Arguments NoneE {X}.

Monadic:

1
2
3
4
5
6
7
8
9
10
11
12
13
14

Notation "' p <- e1 ;; e2"
   := (match e1 with
       | SomeE p ⇒ e2
       | NoneE err ⇒ NoneE err
       end)
   (right associativity, p pattern, at level 60, e1 at next level).

Notation "'TRY' ' p <- e1 ;; e2 'OR' e3"
   := (match e1 with
       | SomeE p ⇒ e2
       | NoneE _ ⇒ e3
       end)
   (right associativity, p pattern,
    at level 60, e1 at next level, e2 at next level).

1
2

Definition parser (T : Type) :=
  list token → optionE (T * list token).

1
2
3
4
5
6
7

newtype Parser a = Parser (String -> [(a,String)])

instance Monad Parser where
   -- (>>=) :: Parser a -> (a -> Parser b) -> Parser b
   p >>= f = P (\inp -> case parse p inp of
                           []        -> []
                           [(v,out)] -> parse (f v) out)

combinator many

Coq vs. Haskell

1. explicit recursion depth, .e. step-indexed
2. explicit exception optionE (in Haskell, it’s hidden behind the Parser Monad as [])
3. explicit string state xs (in Haskell, it’s hidden behind the Parser Monad as String -> String)
4. explicit accepted token (in Haskell, it’s hidden behind the Parser Monad as a, argument)

1
2
3
4
5
6
7
8
9
10
11
12

Fixpoint many_helper {T} (p : parser T) acc steps xs :=
  match steps, p xs with
  | 0, _ ⇒
      NoneE "Too many recursive calls"
  | _, NoneE _ ⇒
      SomeE ((rev acc), xs)
  | S steps', SomeE (t, xs') ⇒
      many_helper p (t :: acc) steps' xs'
  end.

Fixpoint many {T} (p : parser T) (steps : nat) : parser (list T) :=
  many_helper p [] steps.

1
2
3
4
5
6
7
8
9

manyL :: Parser a -> Parser [a]
manyL p = many1L p <++ return []   -- left biased OR

many1L :: Parser a -> Parser [a]
many1L p = (:) <$> p <*> manyL p
-- or
many1L p = do x <- p
              xs <- manyL p
              return (x : xs)

ident

1
2
3
4
5
6
7

Definition parseIdentifier (xs : list token) : optionE (string * list token) :=
  match xs with
  | [] ⇒ NoneE "Expected identifier"
  | x::xs' ⇒ if forallb isLowerAlpha (list_of_string x)
             then SomeE (x, xs')
             else NoneE ("Illegal identifier:'" ++ x ++ "'")
  end.

1
2
3
4

ident :: Parser String
ident = do x  <- lower
           xs <- many alphanum
           return (x:xs)

Step-Indexed Evaluator

…Copied from 12-imp.md:

Chapter ImpCEvalFun provide some workarounds to make functional evalution works:

1. step-indexed evaluator, i.e. limit the recursion depth. (think about Depth-Limited Search).
2. return option to tell if it’s a normal or abnormal termination.
3. use LETOPT...IN... to reduce the “optional unwrapping” (basicaly Monadic binding >>=!)
   this approach of let-binding became so popular in ML family.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

Notation "'LETOPT' x <== e1 'IN' e2"
   := (match e1 with
         | Some x ⇒ e2
         | None ⇒ None
       end)
   (right associativity, at level 60).

Open Scope imp_scope.
Fixpoint ceval_step (st : state) (c : com) (i : nat)
                    : option state :=
  match i with
  | O ⇒ None       (* depth-limit hit! *)
  | S i' ⇒
    match c with
      | SKIP ⇒
          Some st
      | l ::= a1 ⇒
          Some (l !-> aeval st a1 ; st)
      | c1 ;; c2 ⇒
          LETOPT st' <== ceval_step st c1 i' IN    (* option bind *)
          ceval_step st' c2 i'
      | TEST b THEN c1 ELSE c2 FI ⇒
          if (beval st b)
            then ceval_step st c1 i'
            else ceval_step st c2 i'
      | WHILE b1 DO c1 END ⇒
          if (beval st b1)
          then LETOPT st' <== ceval_step st c1 i' IN
               ceval_step st' c i'
          else Some st
    end
  end.
Close Scope imp_scope.

Relational vs. Step-Indexed Evaluation

Prove ceval_step is equiv to ceval

->

1
2
3

Theorem ceval_step__ceval: forall c st st',
      (exists i, ceval_step st c i = Some st') ->
      st =[ c ]=> st'.

The critical part of proof:

• destruct for the i.
• induction i, generalize on all st st' c.
  1. i = 0 case contradiction
  2. i = S i' case;
     destruct c.
     • destruct (ceval_step ...) for the option
       1. None case contradiction
       2. Some case, use induction hypothesis…

<-

1
2
3
4
5
6

Theorem ceval__ceval_step: forall c st st',
      st =[ c ]=> st' ->
      exists i, ceval_step st c i = Some st'.
Proof.
  intros c st st' Hce.
  induction Hce.

Basic Extraction

• OCaml (most mature)
• Haskell (mostly works)
• Scheme (a bit out of date)

1

Extraction "imp1.ml" ceval_step.

When Coq processes this command:

1
2

The file imp1.ml has been created by extraction.
The file imp1.mli has been created by extraction.

Controlling Extraction of Specific Types

如果不做任何处理的话…生成的 ml 里的 nat 则都会是 Church Numeral…

We can tell Coq how to extract certain Inductive definitions to specific OCaml types.
we must say:

1. how the Coq type itself should be represented in OCaml
2. how each constructor should be translated

1

Extract Inductive bool ⇒ "bool" [ "true" "false" ].

also, for non-enumeration types (where the constructors take arguments),
we give an OCaml expression that can be used as a “recursor” over elements of the type. (Think Church numerals.)

1
2
3
4

Extract Inductive nat ⇒ "int"
  [ "0" "(fun x → x + 1)" ]
  "(fun zero succ n →
      if n=0 then zero () else succ (n-1))".

1
2
3

Extract Constant plus ⇒ "( + )".
Extract Constant mult ⇒ "( * )".
Extract Constant eqb ⇒ "( = )".

注意：保证提取结果的合理性是你的责任。

1

Extract Constant minus ⇒ "( - )".

比如这么做很诱人……但是我们 Coq 的定义里 0 - 1 = 0, OCaml 的 int 则会有负数…

Recursor 的理论与实现 - a “encoding” of case expression and sum type

1
2
3
4
5
6

Fixpoint ceval_step (st : state) (c : com) (i : nat)
                    : option state :=
  match i with
  | O => None
  | S i' =>
    match c with

1
2
3
4

let rec ceval_step st c = function
  | O -> None
  | S i' ->
    (match c with

1
2
3
4
5

let rec ceval_step st c i =
  (fun zero succ n -> if n=0 then zero () else succ (n-1))
    (fun _ -> None)     (* zero *)
    (fun i' ->          (* succ *)
    match c with

注意我们是如何使用 “recursor” 来替代 case, match, pattern matching 得。

recall sum type 在 PLT 中的语法与语义：

1
2
3
4
5
6
7
8

T ::= 
  T + T

e ::=
  case e of
    | L(e) => e
    | R(e) => e

1
2
3
4
5
6
7
8
9
10
11
12
13

                 e → e' 
             ------------- (work inside constructor)
             C(e) -> C(e')

                 e → e' 
     -------------------------------   (work on the expr match against)
     case e of ... →  case e' of ...

-----------------------------------------------  (match Left constructor, substitute)
case L(v) of L(x) => e1 | R(y) => e2 → e1 [v/x]

-----------------------------------------------  (match Right constructor, substitute)
case R(v) of L(x) => e1 | R(y) => e2 → e1 [v/x]

可以发现 case 表达式可以理解为一种特殊的 application，会将其 argument 根据某种 tag （这里为构造函数） apply 到对应的 case body 上，
每个 case body 都是和 lambda abstraction 同构的一种 binder：

 L(x) => e1     ===   λx.e1
 R(x) => e2     ===   λx.e2 

 case v e1|e2   ===   (λx.e1|e2) v      -- `e1` or `e2` depends on the _tag_ wrapped on `v`

这个角度也解释了 Haskell/SML 在申明函数时直接对参数写 pattern match 的理论合理性.

根据经验几乎所有的 binding 都可以被 desugar 成函数（即 lambda expression).
难点在于我们如何 re-implement 这个 tag 的 switch 机制?

对于 Inductive nat 翻译到 OCaml int 时，这个机制可以用 v =? 0 来判断，因此我们的 recursor 实现为

1
2
3
4

fun zero succ                (* partial application  *)
  n -> if n=0                (* 判断 tag ... *)
       then zero ()          (* 0   case =>  (λx.e1) v *)
       else succ (n-1)       (* S n case =>  (λx.e2) v *)

我的日常主力编辑器主要是：

• (Neo)Vim
• Spacemacs (via Emacs-plus)
• Visual Studio Code
• IntelliJ IDEA

这里面只有 (Neo)Vim 是存活在终端中的（我并不在终端内使用 Emacs），而由于我日常主要是从终端（via iTerm）来使用电脑，所以会把他们都加入到 $PATH 里以方便从终端中唤起，VSCode 和 IDEA 都有一键加入的功能， Emacs 我在 ~/.zshrc 中放了一个 alias emacs='open -n -a Emacs.app .' 解决。

但是，偶尔也会有从 Finder 中打开文件的需求，这时候如果通常会打开拓展名所绑定的 Open with... 应用，在大部分时候我的默认绑定是 VSCode，但是今天心血来潮觉得有没有办法直接打开 Vim 呢？搜了一下还真有基于 AppleScript 的解决方案：

1. 打开 Automator.app
2. 选择 New Document
3. 找到 Run AppleScript 的 action 双击添加
4. 编写 AppleScript 脚本来唤起终端与 vim （下文给出了我的脚本你可以直接稍作修改使用）
5. 保存为 Applications/iTermVim.app （你可以自己随便取）
6. 找到你想要以这种方式打开的文件，比如 <随便>.markdown，⌘ i 获取信息然后修改 Open with 为这个应用然后 Change All...

效果超爽 ;)

1
2
3
4
5
6
7
8
9
10
11
12
13

on run {input, parameters}
  set filename to POSIX path of input
  set cmd to "clear; cd `dirname " & filename & "`;vim " & quote & filename & quote
  tell application "iTerm"
    activate
    tell the current window
      create tab with default profile
      tell the current session
        write text cmd
      end tell
    end tell
  end tell
end run

我这里的代码是采取是用 iTerm 与唤起 vim、窗口置前、在新窗口中打开、同时 cd 到目录。你也可以改成用 macOS 自带的 Terminal.app、在新窗口而非新 tab 打开、应用不同的 profile、或是执行其他 executable 等……任你发挥啦。

References

• Open file in iTerm vim for MacOS Sierra
• Open file in Terminal Vim on OSX

这篇文章转载自我在知乎上的回答

作为 PWA 在国内的早期布道者与实践者，我觉得挺凉的。
以下都是主观感受且 opinion is my own。

PWA（甚至整个 Web）似乎被 Google（Chrome）与「第三世界」绑到一起去了。「这世界还有多少人没上过网、没有 4G、没有 3G……印度、印度尼西亚、非洲、乌干达……」这便是这两年的 Chrome Dev Summit 的主旋律了。

而这或许也是现在整个 Google 的主旋律吧，于是便成了 Chrome 和 Chrome 的产品经理们的 KPI（OKR），美其名曰「为了互联网的下一个十亿用户」。我不是说关心第三世界这事不好，但问题在于你一边嘴上说着 「Open Web、大家的 Web」，一边身体上却只想着把 Web 变成「你想要的那个 Web」，然后把其他 Web 的发展方向都「耽误」掉了。

PWA 的商业案例至今为止，我感到 legit（正当）的仍然只有 twitter，是真正在按一个「给所有用户都能用」的标准来做的。Airbnb/Pinterest/Spotify 可能能及格，而其他的则要么是商业互吹（吹一波走人），要么就是利益（市场导向）一致（Instagram 以及逐年增多的印度系产品）。

我相信很多开发者和我一样对 PWA 的期待本来是作为 RN/Flutter 等跨平台开发的 alternatives（替代品），结果现在连几年前的 hybrid 方案 Cordova (Phonegap)、Electron的实力都没到， 不要说国内各种自家魔改的 Webview（容器、小程序）了。两年的时间本足以做大量这方面的工作 —— 留学前我还担心是不是两年后我就跟不上 PWA 的发展了，结果现在根本就没什么大动静 —— 每年 CDS 确实都仍然会扔几个新的有关 capability 的 API 出来， 但是跟了这么多年 Chrome Dev Summit 我也算是看清了这秀场的节奏 —— 每年扔出来的东西吧，第二年弃坑 2/3，剩下 1/3 就是遛狗 —— virtual list 说了几年了？类似 portal 这样的 navigation-transition 说了几年了？file system API 说了几年了？我吐槽的点在于，Google（Chrome）你年年画大饼，最后大部分有真正投入资源的，全是你那「第三世界」新兴市场相关的。作为 Web 开发者你一定知道，有多少新 API 落地到我们日常开发了？

Don’t just take my word. 你应该自己去听听这两年的 Chrome Dev Summit，是不是绝大多数的场次都围绕着对「低配」内存、CPU、网络环境的优化 —— 俨然一副「Web 就只适合在这么不行的地方用」的气息，你一个 Web 开发者都要针对 L1/L2 Cache 优化了你说我们怎么不直接写汇编呢？而单纯谈论 CSS/JS 等 Web 技术的发展，不带使用场景 bias 的场次比例一年比一年少。至于 WebAssembly/WebGL/WebXR？—— who TM care? 人家连网都上不了你还想玩 3D/VR 游戏？人家连电脑都没有你还想在 Web 上做生产力工具？WebAssembly 场靠着 Google Research 有点 AI 项目讲了讲 thread 和 SIMD 都能让我感觉到一种与整场会议违和的尴尬……而 3D, VR and AR 总共加起来就做了个六分钟的小短片播，把我乐得。

所谓的 Fugu Project（PWA 项目在 Google 的代号）在我眼里就是 Google「让 Web 成为他们在第三世界的开发平台」而准备的一个项目：官方提及 PWA 最爱提的用户场景不是 Web 的可索引性、可链接性、甚至都不是即开即用（on-demand），而是「用户因为没有流量和 wifi 所以不愿安装原生应用」 。那几个 dev advocate 反正每年就做些 P 用都没有的玩具在那里自娱自乐自 high，做个扫雷游戏然后说我们这个一路支持到功能机用键盘来玩哦……一向亲 JSer 的 Addy Osmani 的 Adaptive Loading 场也来一句「我们要为开 Data Saver（省流量模式、无图模式）的用户做优化！」，这世界大概是又回去到了 WAP 的时代吧……而项目带头人 Alex Russell，即便我仍然很感激您过去对 Web 的影响和贡献，但您这两年来动不动就是「怼框架怼友商怼空气」—— 你们这些垃圾框架，居然要 50 KB！你们这些垃圾开发者，用什么框架，Use the platform！（i.e. 用我们的 Web Component （的框架）！）你们这些垃圾浏览器，还不快点支持我们要的 API！ —— 都是你们伤害了我的 W(K)e(P)b(I)！司马昭之心，路人皆知。

quote @尤雨溪

他们在乎的是「下一个十亿用户」，中国显然不在其中呢

即便你也是 Web 开发者我也是 Web 开发者，但显然我们已经不是 Google（Chrome）想要支持的 Web 开发者了：当无数 Web 开发者起来为 JS 社区在应用框架的先进性上探索，当我们想要证明 Web 在今天的硬件上终于可以挑战 Native，当我们想要在动画和交互上挑战当年的 Flash，当我们认为 Web 技术已经可以胜任众多桌面软件，当社区期待 Web 能够积极跟进下一个新兴技术（whatever that is）甚至担当重任，当国人在谈论着 5G 的到来 Web 开发者应该做什么时 —— 这个当年挟 Web 以令 OS，推动 Web 平台 state-of-the-art 的 Google（Chrome）却变得让我不认识了。

Web 自诞生以来便就是个同床异梦的地方 —— Web 也因此永垂不朽；而对于 PWA 能在当前 Google 的主导下迅速发展成一个有竞争力的跨平台开发解决方案这事儿，或许只是其中的又一黄粱美梦罢了。

补充两点：

• 我支持「小程序」的产品价值，也支持 PWA 作为 Web 开放标准一部分的技术价值。
• PWA 目前主要靠 Google 推动是客观事实，且 PWA 的发展必须依赖平台（浏览器）的参与。

这篇文章转载自我在知乎上的回答

不能，因为是很不一样的心智模型（Mental Model）。我觉得很多同学只关注到了这两套 API 在功能上都能复用逻辑的相似点，而低估了两个框架体系「大背景」上的差异。

正文开始前我先声明一下，

1. 一是本文观点不代表公司。我是觉得圈子里不认同 Hooks 的声音太多了（比如 @徐飞 叔叔、 @贺师俊 贺老、 @题叶 同学等老朋友 no offensive），所以自愿出来平衡一下。

2. 二是我确实好久没有实际写前端了 ，React Hooks 实战还不多，Vue 3 只草草略读了 Composition API RFC 与之前中文的 Vue Function-based API RFC（所以对细节并不太熟悉。）欢迎大家务必指正、补充（与要求补充）。

引言

「框架/库是编程语言上的抽象」，并不意味着框架的设计就无法跳脱出其实现语言的习语（idioms）与编程范式（paradiams）。

得益于 JavaScript 几个非常 Lisp 的特点：一等公民函数、动态类型、一定的宏支持（比如 Babel），这几年前端框架的发展可以看到很多编程语言设计的思路：框架成为了由 DSL 与 API 构成的特定语法（syntax）、从 JavaScript 中扬弃以及由 API 附加的语义（semantics）、支撑这套体系运作的运行时（runtime）、以及所表达的心智模型（mental model）的结合。

Vue 3, “Reactive (Closure-based) OOP”

先来看 Vue（本文中的 Vue 主要指使用 Composition API 下的 Vue）

1
2
3
4
5
6
7
8

const Counter = {
  setup(initialProps) {
    const count = reactive({count: 0}) // or `ref(0)`
    const inc = () => { count.value++ }
    return {count, inc}
  }
  template: "..."
}

Vue 为组件挑选的语义是「对象」：Composition API 的setup 只会调用一次并返回一个对象合并到 Counter 组件上，这个对象与其成员全都是持久的引用，包括保存在 inc 闭包中的状态 count 也是持久的。渲染则是对组件上的template 域的具象化。

Vue 附加的核心语义是（基于可变数据的）「响应式（reactive）」：状态 count 是一个响应式对象，inc 进行状态更改的方式是对 count 直接修改，状态更改的结果是执行所有观察者（watcher）的逻辑，包括重渲染和执行副作用（watchEffect) ，都是基于这个语义纳入数据流。

有的同学（比如题主）说，如果改成返回一个 render 函数，直接利用闭包来保存组件变量，你还说这是对象的语义吗？

1

return (props) => <a onClick={inc}>{count.value}</a>

_是的_。Vue 的实现需要保持这个函数与其闭包的引用不变（referential identity）来满足状态被持久化的语义，是 JavaScript 用闭包模拟对象私有属性的经典模式[1]。（「闭包是穷人的对象，对象是穷人的闭包」）

为了帮助你理解，如果我们有一门假想的 Vue 语言的话……

1
2
3
4
5
6

// hypothetical Vue lang
component Counter (props) {    // constructor
  @reactive count = 0          // field
  inc() { count.value ++ }     // method
  render() { return <a onClick={inc}>{count.value}</a> }
}

是不是有基于类的 OOP 内味了？只不过 Vue 的对象是基于单例（或者闭包）而非类（或原型）实现，以及成员是被施过 reactive 魔法哒！这里我们展示了如何从概念上将 Vue 归约到 OOP 的心智模型，不过需要注意得是，Vue 整个体系（考虑状态管理、数据流控制）的心智模型有很多 FP 的东西在里面，仍然和传统观念（比如 Java）的 OOP 有很大差别，[2][3]。

Vue 运行时的核心是 dependency tracking（依赖追踪），首先它使得 reactive 语义对用户相对 implicit（隐式），依赖都是自动收集的，大大降低了用户的心智负担。其次呢它非常细的跟踪粒度配合 Vue 使用静态化程度比较高模板使得重渲染自动就可以做到非常精准。

总结起来，Vue 在组件方面的心智模型仍然是「拥有数据与行为且自响应式的对象」，只要照着这个思路去想，就比较好理解「为什么 Vue 的状态可以使用可变数据结构」、「为什么 Vue 需要ref 包装值类型」，以及 RFC 在对比 React Hooks 时提到的「为什么 Vue 更接近大家习惯的 JS 」（这点比较主观就是了）、「为什么 Vue 的 GC 压力会更小」、「为什么 Vue 不需要手动声明依赖」等优势的由来了。

React, “Purely (Semi-Monadic/Algebraic) FP”

再来看 React（本文中的 React 主要指 Hooks API 下的 React）

1
2
3
4
5

function Counter(props) {
  const [count, setCount] = React.useState(0);
  const inc = () => setCount(count + 1)
  return <a onClick={inc}>{count}</a>
}

React 为组件挑选的语义是「函数」，每次渲染都是对 Counter 这个函数的一次真实调用。每次 useState 都会执行并从 React 那取出当前的状态给 count，每次也都会创建一个新的 inc 函数（故其闭包中捕获的也是新的 count 值）。

React 附加的核心语义是一个副作用受控的「执行上下文（evaluation context）」，通俗得说就是 React 这个运行环境：状态 count 每次都要从 React 上下文中取出，inc 对状态更改的方式是用 setCount 更新上下文里的内容，状态更改的结果是这个函数会被重新调用，调用时函数就会从新的上下文中获得新的状态、进行重渲染和安排上（schedule）受上下文控制的副作用（useEffect) 。

为了帮助你理解，如果我们有一门假想的 React 语言的话……

1
2
3
4
5
6
7

// hypothetical React lang Ⅰ
component Counter = (props) =>      // function
  @context.state(1) {                  // context provides `get_or` and `put`
    count <- get_or(0)              // get from context (or use default value)
    let inc = () => put(count + 1)  // callback can update the context
    return <a onClick={inc}>{count}</a>
  }

是不是有基于 Monad 的 Haskell 内味了？只不过 React 把 API 做得完全不需要你弄懂这些复杂的东西[4]。如果你不熟悉 Monad 这个纯 FP 的概念，我们可以先不严谨[5]得把它当做文中的「上下文」。扔出 M-bomb 的原因是大家通常把它作为在纯 FP 中处理副作用的标杆，帮助我们展示如何把 React 归约到纯 FP。

有的同学（比如@题叶）会疑惑，这怎么跟我认得的「纯函数」不一样呢，这也是「纯函数式编程」吗？其实如果我们把语法糖展开就会变成：

1
2
3
4
5

component Counter = (props) =>
  context.state(1).get_or(0).then([count, put] => {  // `then` is monadic bind.
    let inc = () => put(count + 1)
    return <a onClock={inc}>{count}</a>
  }).unwrap() // assuming it's safe.

有没有想到同样被称作 Monad，具备异步上下文的 Promise？

再（过度）简化一些，你可以想象成最直白的 state-passing 风格（实际上 2018 年时 React 团队就这么考虑过类似的 API [6]，也是 Seb 的理论基础之一[7]）:

1
2
3
4
5

component Counter = (props, stateMap) => {
  let count = stateMap.get(1, or=0);
  let inc = () => stateMap.set(1, count + 1); // functional update
  return <a onClick={inc}>{count}</a>
}

不过，React 从实现到 API 设计都更靠近与追求[8]的心智模型是一个相对较新的纯 FP 概念 —— Algebraic Effect（代数作用），虽然名字听起来相当迷惑，但其实它在描述副作用上比 Monad 反而更不花哨（少一些 ceremony），理解起来也更加容易，Dan 有一篇给 JSer 看的很易懂的博文[9]并且有中文翻译[10]。我们可以先把它当作「可以重新恢复的 try-catch 」

为了帮助你理解，如果我们又又又又有一门假想的 React 语言的话……

1
2
3
4
5
6
7
8
9
10
11
12
13

// hypothetical React lang Ⅱ
component Counter = (props) => {
  let count = perform getState(1),or=0); // 1. `perform` "throw" effects to the context
                                                // 4. resume with the continuation to here
  let inc = () => perform putState(1, s=count + 1);
  return <a onClick={inc}>{count}</a>
}

// call site
try <Counter /> handle  // 2.try-handle pattern match effects
                        // 3. get state from the context and then resume
| getState(key, or) => resume with context.state(key) ?? or
| putState(key, s) => context.state(key)=s; resume with void

是不是有感觉一些了？我们从组件里「扔出去」去更改 「执行上下文」里的状态，然后再「恢复」回来……

即便 React 已经很努力的降低了 API 的门槛，但其思维的愈加纯函数式确实会在更多程序员眼里非常「离经叛道」。

所以为什么我们需要「纯函数式编程」？抛开大家可能已经熟悉的声明式、数据流清晰、局部推理、易于组合外，其背后的学术理论支撑使得其在编译期静态分析与优化、运行时高并发高并行友好方面都有极高的理论上限和上升空间（近年编程原理的理论研究完全是被函数式编程霸占得）

React 现在运行时侧重的核心是 cooperative multitasking（协作式多任务），来为 React 加入 concurrency（并发）、schedule（调度）等底层能力。很多同学只听说过后端的高并发，其实像多任务操作系统这样的「终极 UI」就是一个高并发且依赖诸如分时（time-slicing）、优先处理（re-priortizing）等进程调度的场景。React 希望把这些技术带给 UI 开发者（比如 Suspense，比如 Selective Hydration，比如 RN 新架构中的 Fabrics），第一步是运行时用 Fiber 架构重写不依赖原生调用栈，第二步就是用 Hooks 解决 Class API 在纯度上约束力不够的问题。不纯的组件在 React 并发模式下很容易出现数据竞态（data race）的问题。

总结起来，React 在组件方面的心智模型是「副作用受上下文托管的纯函数」，只要照着这个思路去想，就比较好理解「为什么 React 中倾向于使用不可变数据结构」、「为什么 useEffect 默认会执行 cleanup 来保持幂等性」、「为什么 React 需要 useRef 这样的跨渲染 ref cell 机制来做 mutable ref 」、「为什么 React 的性能优化是 useMemo, Memo 这样 FP 风格的 memoization 」、「为什么 React 需要 useMemo useCallback 来保持 referential identity 」、「为什么 React 需要用依赖列表来进行 cache invalidation」等问题了。

补充

2016 年底时我就觉得 React 和 Vue 的（一个）终极区别在于「可变」还是「不可变」。

Seb 在 Hooks 发布后收到一些质疑的 brain dump[11] 里写到：

It’s interesting because there are really two approaches evolving. There’s a mutable + change tracking approach and there’s an immutability + referential equality testing approach. It’s difficult to mix and match them when you build new features on top. So that’s why React has been pushing a bit harder on immutability lately to be able to build on top of it. Both have various tradeoffs but others are doing good research in other areas, so we’ve decided to focus on this direction and see where it leads us.

不全部翻译了，说得是整个「大前端」社区里最主要的两条道路分歧：

• 可变 + 变更追踪。包括 Vue，Angular，
• 不可变 + 引用相等性。包括 React，Elm，(Flutter?)

这个分歧其实与我之前行文的侧重点「为组件挑选的语义」其实是对偶的：

• 前者是对传统 Imperative Programming（包括 OOP）思路的一种增强，加入了 Reactivity。
• 后者则是传统 Functional Programming 在 UI 开发领域的发扬光大（Functional Reactive Programming?)，只不过 React 是用一种比较「超越 JS 语言」的方式去实现得。

这两条道路从底子就很不同，所以才造成了 React 和 Vue 在大家眼里的渐行渐远吧。

不过最近多看了一些 Svelte、 SwiftUI[12]和 Jetpack Compose[13]也开始有了一些殊途同归的感觉，Props 无论是跟着 View 销毁还是函数参数总是暂时性的输入，States 无论跟着组件实例还是置外总必须是持久化的，至于怎么判断更新，像 array.push 这种 mutable state 的场景总是不好 track 得，于是就只能各显神通了：React 想通过 reference equality 自动、Vue 3 想通过 Proxy 自动，但其实只要能把 change set 搞出来就行，Vue2/Svelte/SwiftUI/Compose 这些让用户手动给提示得不是也工作得好好得吗？只要能把变更集算出来传递给视图层，那视图层就只管更新（rerender/rebuild/recomposite）就是了。

补充 2

如果是在重度依赖 Flux (Vuex/Redux, whatever) 的场景，可能 Vue/React 会更像是一个只负责渲染的 dumb/passive layer，这种时候上文说的 Vue/React 的差异会显得不明显，因为大部分的状态管理（state management）都已经扔到更外层去做了。

不过，考虑需要组件内聚的场景（即组件自己有私有状态，需要 self-conatined）以及 React Hooks / Vue Composition APIs 开始接管更多（除状态之外的，比如 IO）副作用，这种差异只会变得越来越明显得。

以上。

参考

1. JavaScript 模块化七日谈 - 黄玄的博客 Hux Blog https://huangxuan.me/2015/07/09/js-module-7day/
2. 如何理解尤雨溪在 2019 VueConf 上所讲的 UI 类框架很少使用面向对象的特性这件事？- 黄玄的回答 https://www.zhihu.com/question/328958700/answer/714287394
3. 前端是否适合使用面向对象的方式编程？- 黄玄的回答 https://www.zhihu.com/question/329005869/answer/739525268
4. React Hooks的引入会对之后的React项目开发产生什么影响？- 黄玄的回答 https://www.zhihu.com/question/302916879/answer/536846510
5. React 上下文的组合是通过调用顺序在运行时里维护一个链表而非基于参数化多态的层叠（比如 Monad Transformer）来表达，可以看到都是线性的。
6. State-passing Style Hooks https://mobile.twitter.com/acdlite/status/971598256454098944
7. https://github.com/reactjs/react-basic
8. 可以把上下文或者 Hooks 的调用视为一次 stack unwinding + resume continuation。同样，考虑 row polymorphism 也是线性的。
9. Algebraic Effects for the Rest of Us https://overreacted.io/algebraic-effects-for-the-rest-of-us/
10. 通俗易懂的代数效应 https://overreacted.io/zh-hans/algebraic-effects-for-the-rest-of-us/
11. Why React https://gist.github.com/sebmarkbage/a5ef436427437a98408672108df01919
12. https://swiftwithmajid.com/2019/06/12/understanding-property-wrappers-in-swiftui/
13. https://developer.android.com/jetpack/compose/state#remember

这篇文章转载自我在知乎上的回答

我也看不懂。

对于任何一个我有一定了解的领域，我都知道一大堆我看不懂的东西。反而是对于那些我一点都不了解的，我甚至都说不出来我不懂什么。

有的时候我会觉得，在我眼里还只有前端的时候，我还更自信更爱分享一点。可能因为那时候我能感知到的「边界」就只有 2^4 = 16 这么大，还觉得自己满打满算已经懂了 4 吧。打个比喻的话就是觉得自己已经能干活了，但还想再了解下 JS 引擎、浏览器、框架等的工作原理，或许还想再多学点后端和移动端当个全栈？总之 4/16 已经是「全集」的 25% 了，觉得自己还挺棒棒哒。

结果等我的「知识」真成长到 16 时，才意识到「欧，原来计算机科学还有这么多东西」？而且每个领域水都深得很，教科书里引论文，论文里再引更多论文，像一棵棵树般不断分形出去…认知的「边界」也相应的长到了 2^16 = 65536。自己懂的东西只占 0.02%，一下觉得自己真是什么都不是了。我把这个瞎掰称之为「认知的指数成长理论」。

而我能做的就是学会与这样的认知和平共处。Prof. Matt Might 画的那篇 The illustrated guide to a Ph.D[1]（「博士是什么」) 让我意识到个体在「人类所有知识」面前的渺小，而「成长」的过程，大概就是在那个愈发巨大的「看不懂集」里，挑选出你还愿意继续去「探索」的那些「子集」吧。

「认知的指数成长理论」

作为一个前端。

在相当长的一段时间里，「前端」既是我的兴趣也是我的职业，那时好像不需要有区别 —— 从早早在阿里实习，到还没毕业就在微影带团队，小中大的公司都待过，活动也参加了不少。其实如果就这样专注于「作为一个前端」，应该现在也还混得不赖吧。

可是偏偏你就发现，那个「看不懂集」的边缘总在发着光 —— 群友形容有一部人的动力在于「理解驱动」，我想了想，那或许是我「半路出家」积累的太多疑惑需要解答；又或许，我可能只是想要「旅游」吧 —— 在高三从重点班理科生转了艺术，在阿里从交互又转了前端，可我还有好奇的理论、又或者还没尝试过系统编程，又或者是下一个有趣的产品形态……想去探索下一件事的欲望总是逐渐盖过了舒适感，你听说了那个学科，你听说了那个文明，你听说了风暴中心，可是你不去看，你就永远不知道那里是什么样。

最近多次被问及「前端团队的方向是什么？」才突然意识到自己有一段时间不这样思考了 —— 这个问题天生就带着市场环境强调精细化分工的倾向，而相反地，有时我惊讶于 Facebook 内部「疏于管理」得就像个开源软件的菜市场。前端作为一个子领域当然需要特定的技术设施与人员的专长，但或许你我的职业/兴趣发展、公司的组织架构、软件的开发方式，不一定都非得绑上。

我想要追求的状态不只是能继续做我已经擅长的事情，我还想去探索那些我想要尝试但可能还不太擅长的事情，最后再顺便把钱赚着 —— 就美其名曰「技术自由」吧。所以你说，我是前端吗，我不是前端吗？

「专注」和「职业」又何必要是一个双射呢？

回答。

答题不是我的工作，我不做培训也不靠这个赚钱，不愿花时间琢磨如何哗众取宠，
只是有时恰好有新的感悟可以分享，有时恰好有有趣的题目能引发我的思考；

答题只是博客之外另一个用写作自我沉淀的地方罢了，难免会有点自我，
但反正也只是写给同路人看的，也为了发现与认识更多的同路人；

我不愿意「只」为了答题而写字，也还是希望言之有物，
这道题如此 meta，是回答给谁呢，又或是回答给我呢？

结语。

有的时候需要赚钱，有的时候需要理想。
你是更想做一位黑客与画家，还是想站在 Hilbert 第十问题的肩上。

Gödel 说太难，人生又怎会比 Peano 简单。
面对的 tradeoff 太多，才只能去近似一个想要的模样。

说得都是走心的话，走脑还是多看书吧。
如果能给在读的你带来一点不同思考，那便是对一个碳基生物所能给予的最高嘉奖了。

黄玄，
二〇二〇年七月五日，
于美国圣塔克拉拉。

「有一部分朋友知道，我现在在探索的事情跟前端关系还挺近的啦。
希望我也能突破我自我驱动的局限性，多做一些更落地的事情吧！共勉！」

参考

1. The illustrated guide to a Ph.D http://matt.might.net/articles/phd-school-in-pictures/

雪碧（doodlewind）邀请我给《JavaScript 二十年》 写的推荐序。

JavaScript 常常被戏称为一门偶然成功的玩具语言。而实际上，它出身名门，更是成长在聚光灯之下。纵观历史，有资格被标准化的编程语言甚少，它因此成为多方角力的战场，却也有幸同时得到业界与学界先驱的亲传。时至今日，我们甚至难言是它背负了太多妥协，还是这些妥协才成就了它呢。以史为鉴，或许你会有自己的答案。

— 黄玄，Facebook 软件工程师（编程语言、JS 引擎、前端基础设施）、中文前端社区活跃成员。

本文首发于我的知乎专栏 The Little Programmer，转载请保留链接 ;)

今天微信又刷爆了我的朋友圈 —— 小程序，之前传说的应用号。

不过这篇不谈小程序的技术细节，也不去猜测（因为知道得很清楚……），

也不谈小程序会对中国互联网带来什么影响（自有产品经理会来谈……），

我们说说 Web，the Web。

我们常说的 Web，其实是 World Wide Web 的简称 the Web 的简称。

跟 H5 一样，这货是个简称的简称，所以简到最后就没人知道它本身是个什么意思了。

不要说中国老百姓分不清万维网和互联网了，美国老百姓也一样分不清 Web 和 Internet，

很多不求甚解的从业人士也好不到哪去，Web 常年在技术文章中被翻译得不知所云。

中文世界里把这件事讲得最清楚也最在乎的，非 @不鳥萬如一 莫属了。

比如在《一天世界》博客：微信并不是在「管理」外部链接，因为微信公众号在事实上（de facto）不允许任何外部链接 - 不鳥萬通讯 - 知乎专栏 里他写到：

中文世界一直混淆互联网（internet）和万维网（web）。人们念兹在兹的「互联网开放精神」，实乃万维网的开放精神。万维网的开放主要就体现在一点：任何万维网上的文章之间都可以通过网址随意互相链接。如果我想在文章里介绍 UbuWeb 这个网站，我就可以直接在 UbuWeb 这六个字母上添加它的网址 ubu.com。妳或许觉得这是废话，但在微信公众号的文章里妳做不到；妳只能添加微信生态圈内的链接，比如这个：https://weixin.qq.com/cgi-bin/readtemplate?t=weixin_external_links_content_management_specification（即上述《规范》的链接）

所以如一卸了微信（ 告别微信 一天世界 ）还写了：微信——事实上的局域网 ，嗯，作为一个愈发对 Open Web 这件事 hardcore 的人来说，我是认同的。

如一最在乎的可能是文章，而我更在乎的是应用，Web App。

所谓 Web App，是 Web 的一种进化：从提供文本信息（超文本）到多媒体（超媒体）到提供软件应用服务。硬核的翻译过来大概是“基于万维网的应用”，比如你在 Web 浏览器中使用的 Youtube、Twitter、Medium、Github 等等，它们之间仍然可以通过网址（URL）随意互相链接，遵循 Web 开放标准，并且你几乎可以在任何一个具备浏览器的平台上使用这项服务，因此 Web App 同样是开放的。

如果你听说过 Google 的 Progressive Web Apps，它其实代表的是 Progressive Open Web Apps，只是这样实在太长太啰嗦了。

毕竟，Web 的概念里理应包含着 Open。

（这篇文章的本意并不是为了 advocate PWA，但如果你对 PWA 有兴趣，欢迎阅读： 黄玄：下一代 Web 应用模型 — Progressive Web App​zhuanlan.zhihu.com!

如果说 Hybrid 架构还只是 Web 理想主义的一次让步，那么 React Native 的出现则无疑让部分人的信仰崩塌，然后是 Weex，然后可能是你们猜的微信。

眼见 “以 Web 范式为 Native 平台进行开发” 的方式越来越火，虽然受益的好像是 Web 前端从业人员，可我却不知该不该开心。

我不是说它们是“错误的技术方向”，从实用主义来说它们很棒，很解决问题。

但是，无论他们长得有多像 Web，他们都不是 Open Web 平台的一员。

RN/Weex 根本没有 URL（别跟我说 Universal Links 或 App Links，URL 和 URI 是不同的）

而微信从 JS-SDK 开始，便已经是一个封闭生态了。

这种势头虽然缘起于 Facebook，却更可能在中国撒起野来。

英文世界里对这类事情敏感/hardcore 的人很多，比如写了 Regressive Web Apps 的 Jeremy Keith，因为 PWA 对 URL 不够友好的事情跟 Chrome 开发老大 Alex 吵了一架，而 Alex 也急得说出了：

so, your choices are to think that I have a secret plan to kill URLs, or conclude I’m still Team Web.

要知道，Alex 带着 Chrome 搞 PWA 的原因就是看不爽 Hybrid 破坏了 Open Web。

倘若 Twitter/FB 跟微信一样连链接还不让随便链，大概都得弃用 Twitter，然后像如一一样火冒三丈的写一篇 Byebye Twitter/FB。

而国内天天鼓吹得什么 XX 助力 HTML5 生态，却不知大部分时候这些所谓 “HTML5 生态” 都是和 Web 生态背道而驰的，高下立判。

我开始有些语无伦次了。

在这个 HTML5 与 Web 被极度误用的中文世界里，我也不知道该如何呐喊了。

我只知道，当 Web 只能作为 Native 的 “Markup Language” 存活时，Web 也就不复存在了。

当大家都不跟随 Web 标准自造一套时，Web 所谓的跨平台特性也就烟消云散了。

我之前写过的，Chrome 产品 Leader Rahul 也在 I/O 上说过得：

Web 的 Dicoverable、Linkable、Low Friction、Broad Reach 等等，这些都不是 Web 的本质，Web 的本质是 Open（开放）与 Decentralized （去中心化），这才是万维网（WWW）的初衷，这才是所有这些特性能成立的前提。

Open Web 的信仰让浏览器厂商们重新走到了一起，他们在问你:

Hey, can we make the web great again?