<jupyter_start><jupyter_text>Simply-typed $\lambda$-calculus (STLC)단순타입 람다계산법(Simply-typed $\lambda$-calculus 또는 줄여서 STLC)$\tau \in \textsf{Ty}      ::= \tau_1 \to \tau_2    ~\mid~ \textsf{Int}$$x\in \textsf{Nm} \qquad n\in \textsf{Int}$$e \in \textsf{Expr}   ::=~ x ~\mid~ \lambda x:\tau.e ~\mid~ e_1~e_2 ~\mid~ \\\qquad\qquad ~\mid~ n ~\mid~ e_1 + e_2 ~\mid~ \texttt{if}~e~\texttt{then}~e_1~\texttt{else}~e_0$이렇게 타입있는 람다계산법 문법에서 함수정의식에 나타나는 매개변수 옆에그 매개변수가 가져야 할 타입을 적어 주는 형태가 Church-style이다.즉 위에서 나타난 문법 정의는 Church-style STLC이다.단순타입 람다계산법(STLC)은 실행 전에 타입 검사를 하는 정적 타입 언어의 가장 간단한 형태라 볼수 있다.<jupyter_code>data Ty = Ty :-> Ty | INT  deriving (Eq,Show)
infixr 9 :->

data Expr = Var Nm  | Lam (Nm,Ty) Expr | App Expr Expr
          | Val Int | Add Expr Expr | If Expr Expr Expr
          -- 위에 대해서만 먼저 설명하고 아래의 내용은 과제로
          | Let Nm Expr Expr    -- let x = e2 in e
          | Rec Expr         -- rec (λf:(t2->t).λx:t2.e)
          | LetRec [((Nm,Ty),Expr)] Expr
            {- letrec { x:t1 = e1;        -- e1안에서 x,f,g 모두 사용 가능
                        f:t2 = (\x.e2);   -- e2안에서 x,f,g 모두 사용 가능
                        g:t2 = (\x.e3) }  -- e3안에서 x,f,g 모두 활용 가능
                  in e                
            -}
        deriving Show

type Nm = String
import Data.List 

ppTy (t1 :-> t2) = ppty t1 ++ "->" ++ ppTy t2
ppTy INT = "int"

ppty t@(_ :-> _) = paren (ppTy t)
ppty t           = ppTy t

-- 람다식을 보기좋게 문자열로 변환해주는 함수
ppTm (Var x) = x
ppTm (Lam (x,t) e) = "\\"++x++":"++ppty t++" -> " ++ ppTm e
ppTm (App e1 e2) = pp1 e1 ++ " " ++ pp2 e2
ppTm (Val n) = show n
ppTm (Add e1 e2) = ppp e1 ++ " + " ++ ppp e2
ppTm (If e e1 e0) = "if "++pp2 e++" then "++pp2 e1++" else "++pp2 e0
ppTm (Let x e2 e) = "let "++x++" = "++pp2 e2++" in "++pp2 e
ppTm (Rec e) = "rec "++pp2 e  
ppTm (LetRec ds e) =
    "letrec { "
       ++ intercalate "; " [x++":"++ppty t++" = "++pp2 e | ((x,t),e)<-ds]
       ++ " } in "++pp2 e

pp1 e@(Lam{}) = paren (ppTm e)
pp1 e@(Add{}) = paren (ppTm e)
pp1 e@(If{})  = paren (ppTm e)
pp1 e         = ppTm e

pp2 e@(Var{}) = ppTm e
pp2 e@(Val{}) = ppTm e
pp2 e         = paren (ppTm e)

ppp e@(Var{}) = ppTm e
ppp e@(Val{}) = ppTm e
ppp e@(Add{}) = ppTm e
ppp e@(App{}) = ppTm e
ppp e         = paren (ppTm e)

paren s = "(" ++ s ++ ")"
brack s = "[" ++ s ++ "]"
latex s = "$" ++ s ++ "$"

texTy (t1 :-> t2) = texty t1 ++ "\\!\\to\\!" ++ texTy t2
texTy INT = "\\texttt{int}"

texty t@(_ :-> _) = paren (texTy t)
texty t           = texTy t

-- 람다식을 보기좋게 TeX 코드로 변환해주는 함수
texTm (Var x) = x
texTm (Lam (x,t) e) = "\\lambda " ++ x ++"\\!:\\!"++texty t++ "." ++ texTm e
texTm (App e1 e2) = tex1 e1 ++ "~" ++ tex2 e2
texTm (Val n) = show n
texTm (Add e1 e2) = texp e1 ++ "+" ++ texp e2
texTm (If e e1 e0) = "\\texttt{if}~"++tex2 e++"~\\texttt{then}~"++tex2 e1++"~\\texttt{else}~"++tex2 e0
texTm (Let x e2 e) = "\\texttt{let}~"++x++"="++tex2 e2++"~\\texttt{in}~"++tex2 e
texTm (Rec e) = "\\texttt{rec}~"++tex2 e  
texTm (LetRec ds e) =
    "\\texttt{letrec}~\\{\\,"
        ++ intercalate ";\\;" [x++":"++texty t++"="++tex2 e | ((x,t),e)<-ds]
        ++ "\\,\\}~\\texttt{in}~"++tex2 e

tex1 e@(Lam{}) = paren (texTm e)
tex1 e@(Add{}) = paren (texTm e)
tex1 e@(If{}) = paren (texTm e)
tex1 t         = texTm t

tex2 s@(Var{}) = texTm s
tex2 s@(Val{}) = texTm s
tex2 s         = paren (texTm s)

texp s@(Var{}) = texTm s
texp s@(Val{}) = texTm s
texp s@(Add{}) = texTm s
texp s@(App{}) = texTm s
texp s         = paren (texTm s)
idI = Lam ("x",INT) (Var "x")
idI2I = Lam ("x",INT:->INT) (Var "x")
idII2I = Lam ("x",INT:->INT:->INT) (Var "x")
addTm = Lam ("x",INT) $ Lam ("y",INT) $ Var "x" `Add` Var "y" 

putStr $ ppTm idI
putStr $ ppTm idI2I
putStr $ ppTm idII2I
putStr $ ppTm addTm
putStr $ ppTm (Let "g" idI $ Var "g" `App` Val 3)
putStr $ ppTm (Rec $ Lam ("f",INT:->INT)
                        $ Lam ("x",INT) (Var "f" `App` Var "x"))
putStr $ ppTm (LetRec [(("f",INT:->INT),
                            Lam ("x",INT) $ Var "g" `App` Var "x")
                      ,(("g",INT:->INT),
                            Lam ("x",INT) $ Var "f" `App` Var "x")] 
                $ Var "f" `App` Val 2)
import IHaskell.Display

html . latex $ texTm idI
html . latex $ texTm idI2I
html . latex $ texTm idII2I
html . latex $ texTm addTm
html . latex $ texTm (App idII2I addTm)
html . latex $ texTm (Let "g" idI $ Var "g" `App` Val 3)
html . latex $ texTm (Rec $ Lam ("f",INT:->INT)
                            $ Lam ("x",INT) (Var "f" `App` Var "x"))
html . latex $ texTm (LetRec [(("f",INT:->INT),
                                    Lam ("x",INT) $ Var "g" `App` Var "x")
                              ,(("g",INT:->INT),
                                    Lam ("x",INT) $ Var "f" `App` Var "x")] 
                        $ Var "f" `App` Val 2)<jupyter_output><empty_output><jupyter_text>---- Church-style STLC 타입 규칙인터프리터로 실행할 때는 이름(변수)가 어떤 값에 대응되는지 알 수 있는실행환경($\sigma \in \textsf{Env}$)이 필요했다.타입검사를 할 때는 이름(변수)가 어떤 타입에 대응되는지 알 수 있는타입환경($\Gamma \in \textsf{TEnv}$)이 필요하다.$\displaystyle\textsf{TEnv} ~=~ \textsf{Nm}\xrightarrow{\textrm{fin}}\textsf{Ty}\\\Gamma \in \textsf{TEnv} ::= x_1:\tau_1,\;\ldots\;,\,x_n:\tau_n$$\displaystyle\frac{}{\Gamma \vdash x : \Gamma(x)}\qquad\frac{ x:\tau,\Gamma \vdash e : \tau_2    }{ \Gamma \vdash (\lambda x:\tau.\,e) : \tau\to\tau_2 }\\~\\ \displaystyle\frac{ \Gamma \vdash e_1 : \tau_2\to\tau \quad \Gamma \vdash e_2 : \tau_2     }{ \Gamma \vdash (e_1~e_2) : \tau }\\~\\ \displaystyle\frac{    }{ \Gamma \vdash n : \texttt{int} }\qquad\frac{ \Gamma \vdash e_1 : \texttt{int} \quad \Gamma \vdash e_2 : \texttt{int}    }{ \Gamma \vdash e_1 + e_2 : \texttt{int} }\\~\\ \displaystyle\frac{ \Gamma \vdash e : \texttt{int} \quad       \Gamma \vdash e_1 : \tau \quad \Gamma \vdash e_0 : \tau    }{ \Gamma \vdash \texttt{if}\,~e~\,\texttt{then}\,~e_1~\texttt{else}\,~e_0 : \tau}$<jupyter_code>type TEnv = [ (Nm, Ty) ]

tyinf :: TEnv -> Expr -> Ty
tyinf tenv (Var x) = lookup' x tenv
tyinf tenv (Lam (x,t) e) = t :-> t2
  where
    t2 = tyinf ((x,t):tenv) e
tyinf tenv (App e1 e2) =
  case t1 of
    t2' :-> t  | t2==t2'   -> t
               | otherwise -> error $ show e1 ++" : " ++ ppty t1
                                   ++ " cannot be applied to "
                                   ++ show e2 ++" : " ++ ppty t2
    _ -> error $ show e1 ++ " : " ++ ppty t1
              ++ " is not a function type"
  where
    t1 = tyinf tenv e1
    t2 = tyinf tenv e2
tyinf tenv (Val _) = INT
tyinf tenv (Add e1 e2) =
  case (t1, t2) of
    (INT, INT) -> INT
    (INT, _  ) -> error $ show e2 ++" : " ++ ppty t2 ++ " is not INT type"
    _          -> error $ show e1 ++" : " ++ ppty t1 ++ " is not INT type"
  where
    t1 = tyinf tenv e1
    t2 = tyinf tenv e2
tyinf tenv (If e e1 e0) =
  case t of
    INT | t1 == t0  -> t1
        | otherwise -> error $ show e1 ++" : " ++ ppty t1 ++ " and "
                            ++ show e0 ++" : " ++ ppty t0 ++ " are different type"
    _ -> error $ show e ++" : " ++ ppty t ++ " is not INT type"
  where
    t = tyinf tenv e
    t1 = tyinf tenv e1
    t0 = tyinf tenv e0
tyinf env (Let x e2 e) = tyinf ((x,t2):env) e
  where t2 = tyinf env e2

tyinf tenv e = error $ show e++" type inference is not defined yet"

lookup' x env = case lookup x env of
                  Nothing -> error (x ++ " not defined")
                  Just v  -> v
add1 = Lam ("x",INT) $ Add (Val 1) (Var "x")

html . latex $ texTm add1
html . latex . texTy $ tyinf [] add1
html . latex $ texTm (App add1 (Val 3))
html . latex . texTy $ tyinf [] (App add1 (Val 3))
html . latex $ texTm (App (Val 3) add1)
html . latex . texTy $ tyinf [] (App (Val 3) add1)
html . latex $ texTm (App add1 idI)
html . latex . texTy $ tyinf [] (App add1 idI)
html . latex $ texTm (App idI add1)
html . latex . texTy $ tyinf [] (App idI add1)
html . latex $ texTm (App idI2I add1)
html . latex . texTy $ tyinf [] (App idI2I add1)<jupyter_output><empty_output><jupyter_text>---실행전에 타입검사를 통과하면인터프리터(즉, `eval` 함수)를 실행할 때 맞는 타입인지 실행시간에 반복적으로 검사하지 않아도 된다.<jupyter_code>-- call-by-value evaluator
type Env = [ (Nm, Value) ]
data Value = Clos Env Expr
           | Vint Int
           deriving Show

-- 타입 검사를 통과한 프로그램만 eval로 넘어온다고 가장 
eval :: Env -> Expr -> Value
eval _   (Val n) = Vint n 
eval env (Add e1 e2) = Vint (n1 + n2)
    where
        Vint n1 = eval env e1
        Vint n2 = eval env e2
eval env (Var x) = v
    where Just v = lookup x env
eval env e@(Lam _ _) = Clos env e
eval env (App e1 e2) = eval ((x,v2):env1) e
  where
    Clos env1 (Lam (x,_) e) = eval env e1
    v2 = eval env e2
eval env (If e e1 e0) = if n==0 then eval env e0
                                else eval env e1
  where Vint n = eval env e
-- eval env (Let x e2 e) = eval env (App (Lam (x,undefined) e) e2)
eval env (Let x e2 e) = eval ((x,v2):env) e
  where v2 = eval env e2
-- eval ... -- 나머지 경우는 생략 과제로 ...
-- 이런 식으로 타입 검사를 통과하는 프로그램만
tyinf [("x",INT)] (Var "x")
-- eval 함수로 실행
eval [("x",Vint 5)] (Var "x")
-- 이런 식으로 타입 에러가 나는 프로그램은 eval 에 넘기지 않겠다
tyinf [("x",INT)] (Var "y")<jupyter_output><empty_output><jupyter_text>HW4 (총 100점) * 이름: ???(채점할 때 편리하게 여기에 이름을 작성해 주세요) * 학번: ???????(채점할 때 편리하게 여기에 학번을 작성해 주세요)1. 람다계산법에 조건식과 함수정의식(`Lam`) 및 함수적용식(`App`)까지 포함한 `eval` 함수 작성 (10점)     - 타입 검사(`tyinf`)를 통과한 프로그램이라고 가정하고 불필요한 경우의 수 검사를 줄여서1. `let` 식을 포함한     1. `eval` 함수 작성 (5점)          - 함수 작성 전에 let 식에 대한 실행규칙을 명확히 정의     1. `tyinf` 함수 작성 (5점)          - 함수 작성 전에 let 식에 대한 타입규칙을 명확히 정의1. `rec` 식을 포함한     1. `eval` 함수 작성 (15점)          - 함수 작성 전에 rec 식에 대한 실행규칙을 명확히 정의     1. `tyinf` 함수 작성 (15점)          - 함수 작성 전에 rec 식에 대한 타입규칙을 명확히 정의1. `letrec` 식을 포함한     1. `eval` 함수 작성 (25점)          - 함수 작성 전에 letrec 식에 대한 실행규칙을 명확히 정의     1. `tyinf` 함수 작성 (25점)          - 함수 작성 전에 letrec 식에 대한 타입규칙을 명확히 정의최소한 아래 과제 설명에서 작성한 내용의 테스트의 실행 결과를 반드시 포함해야 점수를 다 받을 수 있다. ---- 예시 프로그램을 통해 알아보는 let, rec, letrec  `let` 식은 지역변수를 하나씩 정의```let x = 3 in x + 5```위 식의 실행 결과는 8 첫번째 방법그런데 사실 위의 식은 `(λx:int. x + 5) 3` 과 똑같은 의미이다.그러니까 일반적으로 `let x = e2 in e`는 `(λx:t2. e) e2`와 같은 의미. (단, `t2`는 `e2`의 타입)  두번째 방법`(λx:t2. e) e2`을 한 단계 더 `eval`로 진행했을 때 어떻게 되겠는가 생각해서 한걸음 더 나가서 정리```eval σ ((λx:t2. e) e2) = eval ({x ↦ v2} ⊎ σ) e  (단, v2 = eval σ e2)```그러니까 ```eval σ (let x=e2 in e) = eval ({x ↦ v2} ⊎ σ) e  (단, v2 = eval σ e2)```<jupyter_code>e001 = Let "x" (Val 3) (Add (Var "x") (Val 5))
:type Let
e001
putStrLn $ ppTm e001
html . latex $ texTm e001
eval [] e001
tyinf [] e001
e002 = Let "x" (Val 3) (Lam ("y",INT) $ Add (Var "x") (Var "y"))
putStrLn $ ppTm e002
html . latex $ texTm e002
tyinf [] e002
eval [] e002<jupyter_output><empty_output><jupyter_text>`rec` 식은 재귀함수를 정의하기 위한 식`rec`이 Z-combinator를 나타낸다고 생각하면 된다.Z-combinator는 일반적으로 타입 검사를 통과하지 못하는 람다식이기 때문에 이렇게 재귀함수를 정의하는 기능을 프로그래밍 언어에 직접 추가해 준다.```rec (λf:(int->int) . λi:int . if i then i + f(i + -1) else i)```위 식은 n을 넘기면 n~0까지 합을 구하는 함수이다.```rec (λf:(int->int) . λi:int . if i then i + f(i + -1) else i) 100rec (λf:(int->int) . λi:int . if i then i + f(i + -1) else i) 999...```매번 이렇게 복붙하면 좀 그러니까 `let` 식과 같이 활용하면 좀 났겠죠?```let sum = rec ( λf:(int->int) . λi:int .                      if i then i + f(i + -1) else i ) in ...    sum 100    ...    sum 999    ...```  첫번째 방법 (이렇게 시도해 볼 수는 있지만 ... 이해하는데 도움은 되는데 ...)실행히 끝나지는 않지만 더 짧은 프로그램인 무한루프인 경우를 생각하면 ```(rec (λf:(int->int) . λi:int . f i)) 2...... 계속 실행해 보다 보면 언젠가 다시 똑같은 곳으로 돌아오지 않을까?...(rec (λf:(int->int) . λi:int . f i)) 2...````rec`로 결국은 어떤 "함수"를 정의하는 것이기 때문에 가장 바깥에 `rec`없이 `(λi:int . ???)` 형태로 똑같은 의미가 되도록 풀어 써보자.```(λi:int . (rec (λf:(int->int) . λi:int . f i)) i) 2...(rec (λf:(int->int) . λi:int . f i)) 2```아하! 그러니까 ```(rec (λf:(int->int) . λi:int . f i)=(λi:int . (rec (λf:(int->int) . λi:int . f i)) i)```즉, `(rec (λf:t->t. e))`는 `e`에 나타나는 `f`를 자기 자신,그러니까 `f`를 `(rec (λf:t->t. e))`로 바꿔친 `(λx:t. e')`와 같은 의미이다!```  eval σ (rec (λf:t->t. e))= eval σ e'                (단, e'는 e안의 f를 (rec (λf:t->t. e))로 바꿔친 녀석)```말로 주저리 주저리 하지 말고 e안의 f를 어쩌고를 람다식으로 그냥 표현할 수 있잖아!!`e'`는  `(λf:t->t. e) (rec (λf:t->t. e))`를 한단계 계산을 진행한 결과!!!```  eval σ (rec (λf:t->t. e))= eval σ ( (λf:t->t. e) (rec (λf:t->t. e)) )  ```그런데 이 방법은 지금 우리가 작성하는 call-by-value 에서는 문제가 생길 수도 있으니 주의!!!(그런데 혹시 될수도 있음 Haskell이 call-by-need라서 동작할 가능성도 있을지도?)  두번째 방법실행히 끝나지는 않지만 더 짧은 프로그램인 무한루프인 경우를 생각하면 ```σ  ,  (rec (λf:(int->int) . λi:int . f i)) 2...{ f ↦  } ,  f 2```만약 rec 가 아니라 그냥 보통 람다로 정의된 함수(`λi:int . f i)`라면그냥 σ' = σ 일텐데 지금은 그러면 곤란 ...다음 단계까지 생각하면  σ'이 무엇인지 답에 가까워진다.```σ' ,  f 2...σ' ,  f 2...```결론적으로``` eval σ (rec (λf:(int->int) . λi:int . f i)) = ```<jupyter_code>e010 = Rec  (Lam ("f", INT :-> INT) . Lam ("i", INT) $
                If (Var "i")
                    (Var "i" `Add` (App (Var "f") (Var "i" `Add` Val(-1)))) -- i + f(i + -1)
                    (Var "i")                                             -- i
            )
e010
putStrLn $ ppTm e010
html . latex $ texTm e010
eval [] (App e010 (Val 100)) -- 1에서부터 100까지 합을 구하도록 실제 재귀함수를 호출 해서 실행시키는 테스트 
tyinf [] e010<jupyter_output><empty_output><jupyter_text>`letrec` 식은 `let`과 `rec`의 기능을 한꺼번에 여러 개를 활용한개만 활용하는 경우```letrec { sum :(int->int) = λi:int . if i then i + sum(i + -1)                                         else i               }   in (sum 100)```지역변수를 한꺼번에 여러 개 가능 ... 그러니까 하는 김에 상호 재귀(mutual recursion)도 ...```letrec { not :(int->int) = λx:int . if i then 0                                         else 1 ;         even:(int->int) = λi:int . if i then not( odd(i + -1))                                         else 1 ;         odd :(int->int) = λi:int . if i then not(even(i + -1))                                         else 0                 }   in odd 7```even과 odd 함수에는 음수가 아닌 정수가 넘어온다고 가정 (아니면 무한루프 도니까 ...)<jupyter_code>e100 = LetRec
        [ (("sum", INT:->INT), Lam ("i",INT) $ If (Var "i")
                                                (Var "i" `Add` App (Var "sum") (Var "i" `Add` Val(-1))) -- i + sum(i + -1)
                                                (Var "i") )                                             -- i
        ]
        (App (Var "sum") (Val 100))

e100
putStrLn $ ppTm e100
html . latex $ texTm e100
eval [] e100
tyinf [] e100
e200 = LetRec
        [ (("not",  INT:->INT), undefined)
        , (("even", INT:->INT), undefined)
        , (("odd",  INT:->INT), undefined)
        ]
        (App (Var "odd") (Val 7))<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.18968058968058968, 'fraction_numerical': 0.027237627237627238, 'mean_word_length': 2.0349382190029823, 'pattern_counts': {'":': 3, '<': 27, '<?xml version=': 0, '>': 90, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 25, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '6', 'dir': 'jupyter-structured-clean-dedup', 'id': '391759', 'license': 'MIT', 'n_tokens_mistral': 7546, 'n_tokens_neox': 8168, 'n_words': 1991, 'path': '08 Simply-typed lambda calculus.ipynb', 'repo_name': 'hnu-pl/pl2020fall', 'size': '14245'}