head関数のいくつかの定義

不正な値は実行時エラーを生じさせる

型安全でない

部分関数になっている

実行時エラーが生じうる

code:定義.hs

head (x:_) = x

head [] = error "empty list"

code:使用.hs

let xs = head [] -- no type error, runtime error

不正な値はダミー値で表現する

例えば以下はいずれもNILを返すが、その違いを値から読み取れない

code:lisp

(car '()) ; 不正な入力なのでNILを返す

(car '(() (1 2 3) (4 5 6)))) ; 先頭要素が空リストなのでNILを返す

(car '(NIL (1 2 3) (4 5 6)))) ; 先頭要素がNILなのでNILを返す

これらを区別したい時、追加でハックが必要になる

code:使用.lisp

(car '())

NIL

code:定義.go

func (l *List) Front() *Element {

if l.len == 0 {

return nil

}

return l.root.next

}

Haskellでやるなら、ダミー値を要求するとか

code:hs

headOr def (x:xs) = x

headOr def [] = def

code:定義.hs

head [] = Nothing

head (x:_) = Just x

全域関数である

型に嘘はない

実行時エラーは起きない

しかし、そうすると結局型の嘘が生じるため、実行時エラーの危険性が再燃する

関数の提供者は楽かもしれないが、利用者は面倒

そもそも空配列を適用できないようにする

型に嘘はない

全域関数である

code:定義.hs

head :: NonEmpty a -> a

head (x :| _) = x

逆は難しい

code:hs

head' = fmap head . nonEmpty

code:hs

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

rev_cons = axiom

gdpHead xs = 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

篩型を用いた定義

code:hs

head :: SizeGreaterThan 0 a -> a

head = Prelude.head . unrefine