xkikeg

「型システム入門」メモ

第3章 型なし算術式

Syntax

BNFで定義したプログラムを自然演繹スタイルの推論規則として記述することができる。注意すべき点は実際には推論規則ではなく推論規則のスキーマ(C++的に言えばテンプレート)であるということ。実際にはメタ変数tには任意の項が入ってくる。 これらの構造に対する深さ、大きさなどを定義している。また、構造的な帰納法を定義している。

Semantics

上の項（プログラムと言ってもいい）がどのような意味を持つかを定義する。ここでは抽象機械を想定して意味を考えていく。 まず、項の意味というのは最終的には値である。とりあえずbooleanを考えるならtrueとfalseが値である。項を値になるまで簡約 (reduction)していくのが評価 (evaluation)ということになるが、この本ではreductionのステップを評価と読んでいる。本の流儀に合わせて評価と呼ぶことにしよう。 ここでも自然演繹スタイルの推論規則として評価関係を考えている。数学的に言う関係とは、例えば2項関係であれば特定のs∈S, t∈Tに対してR(s, t)が言える時のRであった。要は「ある項tを持ってきて評価すると項t'になるよ」ってことだ。

疑問点

xkikeg

{-# LANGUAGE OverloadedStrings #-}

import Control.Applicative
import Data.Binary.Get
import qualified Data.ByteString as BS
import Data.Conduit
import Data.Conduit.Serialization.Binary
import Data.Word

query :: BS.ByteString

xkikeg

{-# LANGUAGE OverloadedStrings #-}
import Data.Conduit
import qualified Data.Conduit.Binary as CB
import qualified Data.Conduit.List as CL

takeWhile' :: Monad m => (a -> Bool) -> Conduit a m a
takeWhile' f = do
  mx <- await
  case mx of
    Nothing -> return ()

xkikeg

import Data.Either
import Control.Monad

failable :: Int -> Maybe Int
failable x = do
  guard $ x /= 0
  guard $ x /= 10
  return $ x + 10

doFailable :: Int -> IO ()

xkikeg

cancel e ->
  e.preventDefault?()
  e.returnValue ?= false

xkikeg

{-# LANGUAGE QuasiQuotes, TypeFamilies, GeneralizedNewtypeDeriving, TemplateHaskell,
             OverloadedStrings, GADTs, FlexibleContexts #-}
import Data.Conduit (runResourceT)
import Database.Persist
import Database.Persist.Sqlite
import Database.Persist.TH
import Control.Monad.IO.Class (liftIO)
import Control.Monad.Logger (runStderrLoggingT)
import Data.Time

xkikeg

{-# LANGUAGE QuasiQuotes, TypeFamilies, GeneralizedNewtypeDeriving, TemplateHaskell,
             OverloadedStrings, GADTs, FlexibleContexts #-}
import Data.Conduit (runResourceT)
import Database.Persist
import Database.Persist.Sqlite
import Database.Persist.TH
import Control.Monad.Logger (runStderrLoggingT)
import Data.Time

share [mkPersist sqlSettings, mkMigrate "migrateAll"] [persistUpperCase|

xkikeg

{-# LANGUAGE QuasiQuotes, TemplateHaskell, TypeFamilies, OverloadedStrings #-}
{-# LANGUAGE GADTs, FlexibleContexts #-}
import Data.Conduit (runResourceT)
import Database.Persist
import Database.Persist.Sqlite
import Database.Persist.TH
import Control.Monad.Logger (runStderrLoggingT)
import Control.Monad.IO.Class (liftIO)

share [mkPersist sqlSettings, mkMigrate "migrateAll"] [persistLowerCase|

xkikeg

{-# LANGUAGE OverloadedStrings, TypeFamilies, TemplateHaskell,
             QuasiQuotes, MultiParamTypeClasses #-}
import Yesod

data UltDest = UltDest

mkYesod "UltDest" [parseRoutes|
/ RootR GET
/setname SetNameR GET POST
/sayhello SayHelloR GET

xkikeg

{-# LANGUAGE OverloadedStrings, TypeFamilies, TemplateHaskell,
             QuasiQuotes, MultiParamTypeClasses #-}
import Yesod

data Messages = Messages

mkYesod "Messages" [parseRoutes|
/ RootR GET