2022/8/17

自己紹介

mrsekut.icon

mrsekut (まる)

業務ではTypeScriptがメイン

Haskellは趣味(実践が乏しい)

オンライン登壇、Haskellイベントでの発表初めてです

リンク付きのオリジナルのスライド資料は以下にあります

何の話をするか

仕様を型で表現する

その嬉しさ

その方法の一例

参考文献 (知っている人向けのネタバレ)

以下のような実装を目指したい

型を見れば仕様がわかる

型を満たすように実装すれば、正しい使い方になる

逆に言うと、間違った使い方ができない

自然に使えるものである

具体例 その1

引数はリスト

そのリストの先頭要素を返す

空リストに適用した時は???

定義1: 不正な値に適用した時は、実行時エラーにする

code:定義.hs

head (x:_) = x

-- head [] = error "empty list"

不正な値(空リスト)に適用した時は、実行時エラーを返す

code:使用.hs

let xs = head [] -- 型エラーはないが、実行時エラー！

部分関数になっている

型が嘘をついている

型が仕様を正しく表現していない

実行時エラーが生じる

code:定義.hs

head [] = Nothing

head (x:_) = Just x

全域関数である

型に嘘はない

実行時エラーは起きない

code:hs

main = do

case x of

Just x -> print x

Nothing -> print "empty"

しかし、実行時エラーの危険性が再燃する

code:hs

fromJust :: Maybe a -> a

fromJust Nothing = error "Maybe.fromJust: Nothing"

fromJust (Just x) = x

定義3: 空リストを適用できないようにする

code:定義.hs

head :: NonEmpty a -> a

head (x :| _) = x

code:hs

全域関数である

型に嘘はない

Entityの型として考えると、もう少しわかりやすくなる

1度の注文では、1つ以上の商品を購入する

(他の情報は今回は不要なので省略)

code:hs

code:hs

data Order = Order { items :: NonEmpty Item }

この時、後者の定義を採用した方が嬉しい

①型で正確に仕様を表現している

②いちいちhandlingせずに済む

③validationの漏れがない

嬉しさ①: 型で正確に仕様を表現している

code:hs

data Order = Order { items :: NonEmpty Item }

(コメントを書くなという主張ではない)

仕様に追従した生きたドキュメントして型が役立つ

仕様が変われば、型を修正すればプロダクト全体で直すべき箇所がわかる

嬉しさ②: いちいちhandlingせずに済む

内部では、これ以降handlingは不要

https://gyazo.com/141c5002b4fd3e5c576a9061e3fe2e18

外部との境界の例

clientからrequestを受け取るところ

DBからデータを取得するところ

etc.

嬉しさ③: validationの漏れがない

じゃあ、外部との境界で、それをチェックすればいいじゃん、とも発想できる

code:境界付近.hs

let

items = getItems -- 外部からデータを取得

result = if isNotEmpty items -- 1個以上あることを確認

then doSomething items -- 後続の処理へ進む

else error "error"

しかし、これはチェックを忘れても型エラーにならない

code:hs

let

items = getItems

result = doSomething items

ここで、型に仕様を込める

「1個以上ある」ことを検証した後に、その情報を型に込める

code:hs

let

items = getItems -- 外部からデータを取得

result = case parseNonEmpty items of -- 1個以上あることを確認し変換

Just items -> doSomething items -- 後続の処理へ進む

Nothing -> error "error"

doSomething :: NonEmpty Item -> Int -- 後続の処理の例

「仕様を満たしている」という情報を型として保持し続ける

他にも細かい仕様があるなら、全てこの境界で検査してしまう

https://gyazo.com/141c5002b4fd3e5c576a9061e3fe2e18

他言語への応用例

上述の話は型システムがあればHaskellでなくとも嬉しさを享受できる

code:ts

import * as t from 'io-ts';

import { nonEmptyArray } from 'io-ts-types'; // fp-tsからのre-export

const Item = t.type({ name: t.string });

const Order = t.type({

items: nonEmptyArray(Item)

});

その言語に備わっている型システムの表現力によって、どれぐらい自然にできるかは異なる

Haskellでは特に追加のハックは必要なく表現できる

仕様を満たした型の具体例

NonZero Int

\a,b -> a \`div\` b

SortedList a

etc.

まとめ

仕様をできるだけ型で表現しよう

その型に属す値が全て仕様通りか？を考える

内部でhandlingが頻発しないので楽

参考文献

応用

code:hs

rev_cons :: Proof (IsCons xs) -> Proof (IsCons (Rev xs))

rev_cons = axiom

gdpHead xs = Prelude.head (the xs)

-- 使用

gdpEndpts :: IO (Int, Int)

gdpEndpts = do

putStrLn "Enter a non-empty list of integers:"

xs <- readLn

name xs $ \xs-> case classify xs of

IsCons proof ->

return (gdpHead (xs ...proof),

gdpHead (gdpRev xs ...rev_cons proof))

IsNil proof -> gdpEndpts

証明を幽霊型として持ち回る