Algebraic Data Types を備えた言語で自前のListを作る例として、下記を見ました。
名前つきパラメータとGADT|プログラング言語Idrisに入門させたい(v0.9)
data List a = Nil | (::) a (List a)
YouTube: Nathan Holland- GADTs and You; Writing Safer Code Using GADTs- λC 2019 5分22秒あたり
type 'a list = | [] | (::) of 'a * 'a list let empty : 'a list = [] let fibs : int list = [0; 1; 1; 2; 3; 5; 8; 13;]
どちらも、空のときと、連結のときを data
もしくは type
で作っています。
Algebraic Data Types を備えた言語に馴染みがないのですが、これはもうそういうものなのでしょうか?
これらの言語に馴染みがないので、質問自体が変かもしれないですが、
- dataやtypeの中に記載するのはこれで十分(多すぎず・少なすぎない)であるとなぜわかりますか?
::
は、dataやtypeの中に書かないといけないのでしょうか?たとえば別途中間演算子
_::_
として作って(作れるのかどうかはこれらの言語に詳しくないので不明ですが)しまってもよいのではないかと思っています。- dataやtypeは最終的に自前のListを返せばよいので、たとえば、最初から1,2,3つ目の要素をListとして返すといったような関数はdataやtypeの中には書けないのでしょうか?仮に書けたとした場合は、書かないものなのでしょうか?(強引ですがオブジェクト指向的にみると(?)、dataやtypeの中にあったほうが、処理がまとまっていてよいようにも思います。
::
連結はdataやtypeの中に書いたので他の連結に似たような処理も中に書いてよいのでは?) - たとえば他にも、Swiftでは、ある型からある型に変換する際は、コンバーターを設けるのではなくて、コンバーターに相当するイニシャライザー(Javaでいうコンストラクタ)を変換元の方に生やして変換しようという流派もあります。そういった考えを使うと、文字列からListに変換するような処理も dataやtypeに書いてもよいのでは?(上記言語で書けるのかどうかはわかってませんが、IdrisならGADTなのでできそう?)などが思い浮かびます