型システム入門を読んでいます（第４回）

ちょいネタです。

前回の最後に「こんなんできたらいいなあ」という話をしていたのを置きに来ました。

let printThrough arg =
    printfn "%A" arg
    arg

// 構文の定義そのまま
type term =
    | TmTrue
    | TmFalse
    | TmIf of term * term * term
    | TmZero
    | TmSucc of term
    | TmPred of term
    | TmIsZero of term
    | Error of string

// 値の評価用のtype
type cterm =
    | Val of int
    | Bool of bool
    | Err of string

// 数値である(nv)
let rec isnumericval = function
    | TmZero -> true
    | TmSucc t1 -> isnumericval t1
    | _ -> false

// なんらかの値である
let rec isval = function
    | TmTrue -> true
    | TmFalse -> true
    | t when isnumericval t -> true
    | _ -> false

// 例外の定義
exception NoRuleApplies

// 構文解析 式の評価
let rec eval1 = function
    | TmTrue -> TmTrue
    | TmFalse -> TmFalse
    | TmZero -> TmZero
    | TmIf(TmTrue,t2,_) -> eval1  t2
    | TmIf(TmFalse,_,t3) -> eval1  t3
    | TmIf(t1,t2,t3) ->
        let t1' = eval1 t1
        eval1 (TmIf(t1',t2,t3))
    | TmSucc t1 ->
        let t1' = eval1 t1
        TmSucc t1'
    | TmPred TmZero  -> TmZero
    | TmPred(TmSucc nv1) when isnumericval nv1 -> eval1 nv1
    | TmPred t1 ->
        let t1' = eval1 t1 
        eval1 (TmPred t1')
    | TmIsZero TmZero -> TmTrue
    | TmIsZero(TmSucc nv1) when isnumericval nv1 -> TmFalse
    | TmIsZero t1 ->
        let t1' = eval1 t1
        eval1 (TmIsZero t1')
    | _ -> raise NoRuleApplies

// 例外拾える版（？）
let rec eval t =
    try eval1 t
    with NoRuleApplies -> Error "NoRuleApplies"

// 値の評価してみたやつ
let calcSucc = function
    | Val n -> Val (n+1)
    | _ -> raise NoRuleApplies

let calcval t =
    let rec calcval' = function
        | TmTrue -> Bool true
        | TmFalse -> Bool false
        | TmZero -> Val 0
        | TmSucc t -> calcSucc (calcval' t)
        | Error s -> Err s
        | _ -> raise NoRuleApplies
    
    try calcval' t
    with NoRuleApplies -> Err "NoRuleApplies-calcval"

[<EntryPoint>]
let main argv = 

    TmZero
    |> TmSucc
    |> TmPred
    |> TmSucc
    |> printThrough
    |> eval
    |> printThrough
    |> calcval
    |> printfn "%A"

    printfn ""

    let condition = 
        TmZero
        |> TmSucc
        |> TmPred
    
    TmIf(TmIsZero condition,TmTrue,TmFalse)
    |> printThrough
    |> eval
    |> printThrough
    |> calcval
    |> printfn "%A"

    printfn ""

    TmZero
    |> TmIsZero
    |> printThrough
    |> eval
    |> printThrough
    |> calcval
    |> printfn "%A"

    printfn ""

    TmZero
    |> TmSucc
    |> TmSucc
    |> TmSucc
    |> TmSucc
    |> TmSucc
    |> TmSucc
    |> TmSucc
    |> printThrough
    |> calcval
    |> printfn "%A"

    0 // return an integer exit code

初手・コード全文貼り付け。

前回からかわったのはこのへんですね。

// 値の評価用のtype
type cterm =
    | Val of int
    | Bool of bool
    | Err of string

～略～

// 値の評価してみたやつ
let calcSucc = function
    | Val n -> Val (n+1)
    | _ -> raise NoRuleApplies

let calcval t =
    let rec calcval' = function
        | TmTrue -> Bool true
        | TmFalse -> Bool false
        | TmZero -> Val 0
        | TmSucc t -> calcSucc (calcval' t)
        | Error s -> Err s
        | _ -> raise NoRuleApplies
    
    try calcval' t
    with NoRuleApplies -> Err "NoRuleApplies-calcval"

この実装がよい実装なのか全然わからないんですけど、
数値の型と真偽値の型を用意して突っ込みました。

calcSuccはValの中身だけに計算するのスマートにできんぞ？？となってしまったので関数化しています。

あと、eval1も前回と比べて改善しました。
| TmIf(TmTrue,t2,_) -> t2を| TmIf(TmTrue,t2,_) -> eval1 t2にしたりして、
最終段階（？）まで式を評価するようにしています。

実行結果はこんなん。
スマートな実装かどうかはほんとわからんままですが、「7」とか出たのでニヤついております。

はて、今回はそれだけです。

5章からはラムダ計算です。
パズルっぽくなっていてなかなか難しいかんじでやっています。がんばれ自分。

では！