The Little MLer 筆記

ch0: 執行環境

想用wsl來跑sml的話，poly/ml是不錯的選項

ch1: 定義type

datatype num = ZERO | ONE_MORE of num
datatype ‘a Slist = NIL of ‘a | SCONS of ‘a Slist

ch2: 寫function

datatype Abc = A | B of Abc | C of Abc

fun only_B(A) = true
    | only_B(B(x)) = only_B(x)
    | only_B(C(x)) = false
(only_B : Abc -> bool)

datatype ‘a Xyz = X of ‘a | Y of ‘a Xyz | Z of ‘a Xyz
fun is_xy(X(x)) = true
    | is_xy(Y(x)) = is_xy(x)
    | is_xy(Z(x)) = false
(is_xy : ‘a Xyz -> bool)

ch3: 在list上遞迴

fun rem_B(A) = A
    | rem_B(B(x)) = rem_B(x)
    | rem_B(C(x)) = C(rem_B(x))
fun C_in_fron_of_B(A) = A
    | C_in_fron_of_B(B(x)) = C(B(C_in_fron_of_B(x)))
    | C_in_fron_of_B(C(x)) = C(C_in_fron_of_B(x))

fun subst_B_C(x) = rem_B(C_in_fron_of_B(x))
(* OR *)
fun subst_B_C(A) = A
    | subst_B_C(B(x)) = C(subst_B_C(x))
    | subst_B_C(C(x)) = C(subst_B_C(x))
(* 都是走訪同一list故可以用同一種走訪，把兩個式子結合起來(map fusion) *)

ch4: tuple & 多參數function

(A,X,A) :: (Abc * Xyz * Abc)

datatype Abc = A | B | C

fun add_a(A) = (A,A)
    | add_a(B) = (B,A)
    | add_a = (C,A)
(add_a : Abc -> (Abc * Abc))

可以利用type variable來打少一點字

fun add_a(x) = (x * A)
(add_a : ‘a -> (‘a * Abc))

這個比較抽象，但是比較詳細的(照著datatype產生的fun)可以找出更多可能的錯誤

fun has_a(a:Xyz, A, b:Xyz) = true
    | has_a(a:Xyz, b, b:Xyz)) = false
(has_a : (Xyz * Abc * Xyz) -> bool)

ch5: type的參數可以不只一個

type的參數可以不只一個

datatype ‘a De = D | E of (‘a * (‘a De))

datatype Abc = A | B | C

fun rem_a(D) = D
    | rem_a(E(A,x)) = rem_a(x)
    | rem_a(E(B,x)) = E(B,rem_a(x))
    | rem_a(E(C,x)) = E(C,rem_a(x))

(* shorter version *)
fun rem_a(D) = D
    | rem_a(E(A,x)) = rem_a(x)
    | rem_a(E(y,x)) = E(y,rem_a(x))

抽象與組合數

輸入的維度上升，pattern的數量(組合數)上升

fun rem(x,D) = D
     | rem(A,E(A,y)) = rem(A, y)
     | rem(A,E(x,y)) = E(x,rem(A, y))
     | rem(B,E(A,y)) = rem(B, y)
     | rem(B,E(x,y)) = E(x,rem(B, y))
     | rem(C,E(C,y)) = rem(C, y)
     | rem(C,E(x,y)) = E(x,rem(C, y))
(rem : (Abc * Abc De) -> Abc De)

把其中一個維度抽出來，像

fun eq_Abc(A,A) = true
     | eq_Abc(B,B) = true
     | eq_Abc(C,C) = true
     | eq_Abc(x,y) = false
fun rem(x,D)         = D
     | rem(x,E(y,z)) = if eq_Abc(x,y)
                       then rem(x,z)
                       else E(y,rem(x,z))

ch6: 樹形遞迴

datatype tree = E | L of Abc * tree | S of tree * tree
datatype ‘a tree = E | F of ‘a * ‘a tree | S of ‘a tree * ‘a tree

fun occur_Abc(a,E) = 0
    | occur_Abc(a,L(b,x)) = if eq_Abc(a,b) then 1+occur_Abc(a,x) else occur_Abc(a,x)
    | occur_Abc(a,S(x,y)) = occur_Abc(a,x) + occur_Abc(a,y)

sexp & slist

datatype ‘a SList = NIL | SCONS of ‘a Sexp * ‘a SList
and
	       ‘a Sexp = ATOM of ‘a | SLIST of ‘a SList

fun occur_Abc_SL(a,Nil) = 0
    | occur_Abc_SL(a,SCons(x,y)) = occur_abc_SE(a,x) + occur_abc_SL(a,y)
    and
fun occur_Abc_SE(a,Atom(b)) = if eq_Abc(a,b) then 1 else 0
    | occur_Abc_SE(a,Slist(x)) = occur_Abc_SL(a,x)

先展開occur_Abc_SE

fun occur_Abc_SL(a,Nil) = 0
    | occur_Abc_SL(a,SCons(Atom(x),y)) = if eq_Abc(a,b) then 1 + occur_abc_SL(a,y) else 0 + occur_abc_SL(a,y)
    | occur_Abc_SL(a,SCons(Slist(x),y)) = occur_abc_SL(a,x) + occur_abc_SL(a,y)

其實SCons的部分都長的很像，做抽象與合併 !!

fun eq_Abc_atom(a,Atom(b)) = eq_Abc(a,b)
    | eq_Abc_atom(a,Slist(b)) = false
fun occur_Abc_SL(a,Nil) = 0
    | occur_Abc_SL(a,SCons(x,y)) = if eq_Abc_atom(a,x) then 1+occur_abc_SL(a,y) else occur_Abc_SE(a,x) + occur_abc_SL(a,y) 
    and
fun occur_Abc_SE(a,Atom(b)) = 0
    | occur_Abc_SE(a,Slist(x)) = occur_Abc_SL(a,x)

ch7: first-order function & stream

first-order function & type inference

fun true_mk(x) = true
(true_mk : ‘a -> bool)
datatype B_or_I = HOT of bool | COLD of int

fun help(f)
     = Hot(true_mk(
	if true_mk(__)
	then f
	else true_mk))
(help : ? -> B_or_I)

f的type是什麼? then part與else part的type要一樣，故f的type是’a -> bool

stream

datatype chain = LINK of (int * (int -> chain))

這裡是把function包上datatype，這樣可以把遞迴藏起來，因為是datatype的關係，在使用時一定要先打開來，才可以做下一個動作。

fun ints(n) = LINK(n+1, ints)
fun skips(n) = LINK(n+2, skips)
fun some_ints(n) = if is_mod_5_or_7(n+1) then LINK(n+1, some_ints) else some_ints(n+1)

上面是產生stream的起點，接著要get stream的值

fun chain_item(n,Link(x,f)) = if eq_1(n) then x else chain_item(n-1,f(n))

如果有個is_prime

fun primes(n) = if is_prime(n+1) then LINK(n+1, primes) else primes(n+1)

fib 是一定要的

fun fibs(n)(m) = LINK(n+m, fibs(m))
(fibs : int -> (int -> chain))
fun fibs_1(m) = LINK(1 + m, fibs(m)) ( == fibs(1))

ch8: curried

fun in_range_c(s,l)(x) = if less_then(s,x) then less_than(x,l) else false
(in_range_c : (int * int) -> (int -> bool))

fun combine(Nil,Nil) = Nil
    | combine(Nil,Cons(a,x)) = Cons(a,x)
    | combine(Cons(a,x),Nil) = Cons(a,x)
    | combine(Cons(a,x)),Cons(b,y)) = Cons(a,combine(x,Cons(b,y))

fun combine(Nil,y) = y
    | combine(Cons(a,x)),y) = Cons(a,combine(x,y))

第一種寫法把所有組合列出來而第二種是只處理一個維度，剩下遞迴

而curried後

fun combine_c(Nil)(y) = y
    | combine_c(Cons(a,x))(y) = Cons(a,combine_c(x)(y))

可以想像成

combine_c(Cons(1,Cons(2,Nil))) => \y -> Cons(1,combine_c(Cons(2,Nil))(y))

所以curried的另一種寫法

fun combine_s(Nil) = fn l2 => l2
    | combine_s(Cons(a,x)) = fn l2 => Cons(a, combine_s(x)(l2))

ch9: exception

datatype box = Bacon | lx of Int
exception No_bacon of int

fun where_is(Nil) = raise No_bacon(0)
    | where_is(Cons(a,x)) = if is_bacon(a) then 1 else 1+where_is(x)

(* where_is(..) handle No_bacon(n) => n *)

exception Out_of_range
fun list_item(n,Nil) = raise Out_of_range
    | list_item(n,Cons(b,rest)) = if eq_int(n,1) then b else list_item(n-1,rest)

fun find(n, boxes)
    = (check(n,boxes,list_item(n,boxes)) handle Out_of_range => find(n div 2, boxes))
and
      check(n,boxes,Bacon) = n
    | check(n,boxes,lx(i)) = find(i,boxes)
fun path(n, boxes)
    = Cons(n,(check(n,boxes,list_item(n,boxes)) handle Out_of_range => path(n div 2, boxes)))
and
      check(n,boxes,Bacon) = n
    | check(n,boxes,lx(i)) = path(i,boxes)

這裡的重點是 [X.. (A.. handle _ => B)]，當excepption發生時被接住時，此時會變成[X.. B]。

ch10: module system in ML

(* interface *)
signature N = 
sig
    type number
    exception Too_small
    val succ : number -> number
    val pred : number -> number
    val is_zero : number -> bool
end;

(* class *)
functor NumberAsNum() (* 傳入functor需要的參數(structure)與一些constraint(對內的type暴露) *)
    :> (* implements *)
    N
=
    struct (private and implement signatrue)
    datatype num = Zero | One_more_than of num
    type number = num
    exception Too_small
    fun succ(n) = One_more_than(n)
    fun pred(Zero) = raise Too_small | pred(One_more_than(n)) = n
    fun is_zero(Zero) = true | is_zero(foo) = false;
 end;

(* object *)
structure NumStruct = NumberAsNum();

另一個plus

signature P =
sig
    type number
    val plus : number*number -> number
end;

functor PON(structure a_N : N)
    :>
    P
=
struct
    type number = a_N.number
    fun plus(n,m) = if a_N.is_zero(n) then m else a_N.succ(plus(a_N.pred(n),m))
end;

structure NumArith = PON(structure a_N = NumStruct);

哪兩個可以一起用嗎?

NumArith.plus(Zero, One_more_than(Zero));

我們不知道NumArith的number是什麼!!

要處理這個問題有三個方法

加入box與unbox的function

signature N_C_R =
sig
    type number
    exception Too_small
    val conceal : int -> number
    val succ : number -> number
    val pred : number -> number
    val is_zero : number -> bool
    val reveal : number -> int
end;

(* NumStruct.reveal( NumArith.plus( NumStruct.conceal(1), NumStruct.conceal(2))); *)

用where把type暴露出來

functor PON(structure a_N : N)
:>
P where type number = a_N.number
=
struct
    type number = a_N.number
    fun plus(n,m) = if a_N.is_zero(n) then m else a_N.succ(plus(a_N.pred(n),m))
end;

functor NumberAsInt2()
:>
N where type number = int (* 這邊的int是refer到外面的env，不會碰到struct .. end 中的東西，*)
=
struct
    type number = int
    exception Too_small
    fun succ(n) = n + 1 fun pred(n) = if n=0 then raise Too_small else n-1
    fun is_zero(n) = n=0
end;

sharing type標出兩個type要一樣

signature J =
sig
    val new_plus : int*int -> int
end;

functor NP(structure a_N : N_C_R
           structure a_P : P
           sharing type a_N.number = a_P.number)
    :>
    J
=
struct
    fun new_plus(x,y) = a_N.reveal( a_P.plus( a_N.conceal(x), a_N.conceal(y)))
end;

structure NPStruct = NP(structure a_N = NumberAsNum()
    structure a_P = PON(structure a_N = a_N));

小總結

functor <<name>>(args with some relations(A.b is equal to B.c, 這也是為什麼fuctor的參數要named的理由)) 
    :>
    <<sig(return type) with some relations(this type is same as ...)>>
=
struct
    code
end;

Y in ML

Y的重點是有一個(g g)這是無限遞迴的，所以要中斷他。在第七章的stream(chain)中就利用datatype來打斷無限遞迴，所以這裡也要用相同的技巧。與chain不同的是，我們的函數的參數是自己，所以不用像chain要多一格來存apply到函數的參數。所以只要存自己就夠了

datatype 'a T = INTO of 'a T -> 'a

fun Y(f)= H(f)(INTO(H(f)))
and H(f)(a) = f(G(a))
and G(INTO(a))(x) = a(INTO(a))(x);

fun mk_fact(fact)(n)
    = if n=0
        then 1
        else n*fact(n-1);

ch0: 執行環境#

ch1: 定義type#

ch2: 寫function#

ch3: 在list上遞迴#

ch4: tuple & 多參數function#

ch5: type的參數可以不只一個#

type的參數可以不只一個#

抽象與組合數#

ch6: 樹形遞迴#

sexp & slist#

ch7: first-order function & stream#

first-order function & type inference#

stream#

ch8: curried#

ch9: exception#

ch10: module system in ML#

小總結#

Y in ML#