Neverについて

この記事は、わりとなんか質問があったので、それを軽くまとめます。

elmのコードを書いていると、Html.programなんていう関数があって、その型は

program : { init : (model, Cmd msg), 
            update : msg -> model -> (model, Cmd msg), 
            subscriptions : model -> Sub msg, 
            view : model -> Html msg } -> 
          Program Never model msg 

となっておりまして、最後のNeverとは一体なんぞや?みたいな質問が多いので、それを軽くまとめようと思います。

Neverとは?

Neverとは一言で言ってしまえば、値が無い型のことです。そんなことを言うと、Maybe aのNothingとかとごっちゃになるという人がいるかもしれませんが、NothingはあくまでMaybe aの値であって、NeverはNeverという型に対応する値がないということです。

elm packageのBasic につぎのように書いてます。

type Never

A value that can never happen! For context:

The boolean type Bool has two values: True and False
The unit type () has one value: ()
The never type Never has no values!

つまりですね、値がないってことはたとえば、Boolだと、2つの値、TrueとFalseがあって、Unit Typeは()という一つの値がありまして、Neverは値はありません!!!!!

ということですね。

さてさてNeverの型はどのように作られているのでしょうか? ということで、Neverの定義を見てみましょう。Basicの実装をとってくると

type Never = JustOneMore Never

ほむほむ。では、JustOneMoreという、コンストラクタがあるんで、Neverの型がつくれるんじゃ?とか思いますが、

tryToCreateNever : Never 
tryToCreateNever = 
 JustOneMore (JustOneMore (JustOneMore ... ))

となり、Neverが再帰的定義になっており、ずーっと型が再帰して値が定義できません。また、Never自体は、opaque typeなので、そもそもこんな定義じゃなくても、neverの値を作る手段は我々にはありません。

Neverのどこが良いのよさ?

とここまで書くと、Neverのについて有効性が気になりますよね。だって、Neverの型の値がないんだもの。どうつかうのよさ?ってなりますよね?

というかそもそも、値がつくれないんだから、どうやってコードに書くのさ?って疑問があるかもしれません。Neverはそもそも、Never単体で記述することはありません。型引数として用います。

たとえば、Maybe a型を考えてみましょう。絶対にNothingを返す、関数を書いてみます。

definitelyNothing : a -> Maybe Int 
definitelyNothing _ = Nothing

さて、この関数は必ずNothingを返します。その返り値の型をMaybe Intとしました。しかし、Maybe Intとする理由はとくにはありません。ただ、Nothingを返すためだけの目的として、Intをつかっただけです。

このときにNeverをつかいます。

definitelyNothing : a -> Maybe Never
definitelyNothing _ = Nothing

さて、上記の2つのコードはどう違うのでしょうか? 違いは、たとえばJustを許容するかどうかの違いにあります。つまりMaybe Intだと、Just 10などを許容してしまうかもしれませんが、Maybe Neverだと、Justの値は取れません。つまり、それだけ、Never型によって関数が制限されています。

もうひとつ例を上げましょう、つぎにResult型を考えてください。

type Result error value = Ok value | Err error

Result型は、成功(Ok)や失敗(Err)を表わします。それが考えられるものを考えます。しかしながら、時には、絶対に成功するけど、Resultで表わしたいときがあります。この場合、Result error valueのerrorの型に値なんて考えられません。このときにNeverを使えます。たとえば、aを取って、絶対にOkを返したいのであれば、次のようにします。

definitelyOk : a -> Result Never a 
definitelyOk a = Ok a

また、たとえば次のような関数があったとしましょう。

exampleFunc : (x -> b) -> (a -> b) -> (Result x a) -> b

とりあえず、実装は考えてませんが、(x -> b)と(a -> b)、Result x aを取り、bを返す関数です。もし、ここで、Resultの型が絶対にOkだけを返すと考えるとすると,

exampleFunc : (a -> b) -> (Result Never a) -> b

と定義できるかもしれません。ここで、気づいて欲しいのは,xという型引数がなくなり、関数としてシンプルになったのではないでしょうか?

最後に冒頭に,紹介したHtml programですが、まずprogramWithFlagsの関数があり、

programWithFlags : { init : flags -> (model, Cmd msg), 
                     update : msg -> model -> (model, Cmd msg), 
                     subscriptions : model -> Sub msg, 
                     view : model -> Html msg } -> 
                   Program flags model msg

このflagsの型引数がなくなったバージョンがHtml programです。

program : { init : (model, Cmd msg), 
            update : msg -> model -> (model, Cmd msg), 
            subscriptions : model -> Sub msg, 
            view : model -> Html msg } -> 
          Program Never model msg 

上記を見比べていると、Programの型にはflagという型引数があるのですが、programの関数の戻り値の型はflagを持たないProgramのであることを表わしており、programWithFlagと比較すると、flagを持つ持たないとで、引数のinitの型が異なることがわかると思います。つまり、flagを持つか持たないかを、Neverを用いることによって型で表現して、関数の型を厳格にしているんですね。

flagに関して詳しくは、https://guide.elm-lang.org/interop/javascript.html を参照してください。

まとめ

最後に簡単にまとめましょう。

• Neverは、値の無い型である。
• Neverを型引数に使うことによって、型が厳格になったり、シンプルになったりする。

以上です。