1. konn-san.com 建設予定地
  2. Blog
  3. GHC 7.4.1 の型レベル新機能を使い倒す 〜GADTs、型族 と DataKinds、ConstraintKinds の円環〜

GHC 7.4.1 の型レベル新機能を使い倒す 〜GADTs、型族 と DataKinds、ConstraintKinds の円環〜 konn-san.com

  • このエントリーをはてなブックマークに追加
posted on 2012/06/07 00:48:45 JST

型であそぼう！

みなさん今日は！遂にHaskell Platform 2012.2.0.0 がリリースされましたね！

そこでこの記事では、シンプルな例を通して、GADTs や型族、更には GHC 7.4.1 の新機能であるデータ型の昇格と制約カインド、などといった型レベルプログラミングの機能を紹介していきたいと思います。こちらが題材となるソースコードです。

問題：リストの要素を関数に渡したい

Haskell を学びたての頃によくしがちな間違いとして、リストの要素を関数に適用したくなると云うことがあるんじゃないでしょうか。どういうことかと云うと、例えば下のような関数があるとしましょー。 

catThreeFiles :: FilePath -> FilePath -> FilePath -> IO String

つまり三つのファイルを結合する関数ですね。 こいつを使って、コマンドライン引数を三つ取って、そのパスの内容を読んで連結するプログラムを書きたかったとします。引数の数は必ず三つ渡されると仮定すると、普通なら 

main :: IO ()
main = do
  [f1, f2, f3] <- getArgs
  putStrLn =<< catThreeFiles f1 f2 f3

などと書くと思いますが、foldl などを覚えたてだと、「catThreeFiles に f1, f2, f3 を順繰りに適用していけばいいんだから、こう書けるんじゃないか……？」と、 

foldl ($) catThreeFiles =<< getArgs

などと書いて「型が合わねーよ！」と叱られる訳です。

foldlを使うことは出来ませんが、この「リストの要素を順次関数に適用する」と云うのを、GHC 7.4.1 の最新機能を使って実現してみたいと思います。

まずおまじない

では早速書き始めましょう。以下で使う言語拡張とモジュール群は以下の通りです。 

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, ConstraintKinds #-}
{-# LANGUAGE TypeOperators, ScopedTypeVariables #-}
module Main where
import GHC.Exts (Constraint)
import Control.Applicative

方針

さて、関数にリスト要素を喰わせるといっても、幾つか問題があります。それは、

  1. どこまでを引数、どこからを返り値とするか？
  2. リストは同一型しか含まないが、関数の引数は異なる型を取り得る

と云うことです。一番目の問題はどういうことかと云うと、Haskell はカリー化があるので、 

withFile :: FilePath -> IOMode -> (Handle -> IO r) -> IO r

みたいな関数があったときに、(Handle -> IO r)までが引数で返り値がIO r である関数と見ることも出来ますし、それともFilePathだけが引数で、IOMode -> (Handle -> IO r) -> IO r が返り値だと見ることも出来ます。

一般に、どちらの場合を採用したいかは用途によって違うので、ここでは引数一覧と返り値を明示したようなデータ型 NAry を定義してみましょう。完全適用の形になって返り値だけになっている状態と、まだ引数を必要としている状態が区別出来ていればよさそうです。

引数を受け付けるような場合はどうあらわせばいいでしょうか？型引数として、関数の引数の型一覧を持たせることが出来るとよいのですが……そんな時に便利なのが、GHC 7.4.1 の新機能、データ型の昇格機能（DataKinds 言語拡張）です。

実装の前に：カインドの説明

データ型の昇格、と云うのは、通常のデータ型を自動的にカインドに持ち上げてくれる機能です。……カインドって何？と云うことで、実装に入る前にカインドについての簡単な説明をしておこうと思います（知っている、と云うひと は飛ばしてしまって構いません）。

GHC 7.4 以前のカインドの世界

カインドと云うのは、型の型のようなものです。なので、型の類推で考えると分かり易いです。

例えば、"こんにちわーるど！" や Just True のように関数ではない、完全に適用された値 は、それぞれ String型、 Maybe Bool型を持ちます。 これと同様に、Int や Maybe Bool のように完全適用の形になっている、カインド を持つ、とされます。つまり、Int :: 、Maybe Bool :: *です。完全適用の形になっている、と云うのは、直感的には「その型を持つ値が存在する」と云う意味だと思っておけばよいです 1。

一方、値の世界には、odd :: Int -> Bool や (++) :: [a] -> [a] -> [a] のように、何らかの引数を取って値を返すような関数があり、これらは引数の型と返り値を ->（アロー）で区切って型が与えられます。 これと似たように、何らかの型を取って違う型を返すような型のカインド（ややこしいですね！）も、アローを使って表現されます。例えば、Maybe 型はそれ自身では値を持たず、他の カインドの型（例えば Int）を取って始めて値を持ちます。そこで Maybe のカインドは -> となります。同様に、 [a] == [] a に注意すれば、[] :: -> ですし、Either は Either Bool Int のように カインドの型を二つ取って値を持つ型を返すので、Either :: * -> * -> * です。

注意が必要なのは、型 Int -> Bool の カインド は である、と云うことです。一瞬 -> のようなカインドを持つように思えるかもしれませんが、Int -> Bool は例えば odd 関数のように 値を持つ のでカインド を持つことになる訳です。

すこしややこしいですね……。まあ、迷ったら、GHCi を開いて :kind コマンドで型のカインドが調べられるので、色々な型のカインドを見てみるとよいでしょう。 とまれ、GHC 7.4.1 以前の世界には * と -> を使って作られるカインドしかなかったと思っておけば問題ないです2。

データ型の昇格とは何者なのか？

さて、GHC 7.4.1 からは、上の基本的なカインドに加えて、DataKinds機能拡張を有効にすることで自前のカインドを定義出来るようになりました。

定義出来る、と云っても無節操に定義出来る訳ではなく、既存のデータ型をカインドに昇格させることが出来るようになった、と云ったほうが正確です。既存の型をカインドに、データコンストラクタを型に持ち上げることが出来るようになったのです。

エッ、どういうこと……？ 掻い摘んで説明しましょう。例えば以下のような自然数を表すデータ宣言があったとします。 

data Nat = Zero | Succ Nat

この時、上で定義されている Nat 型 と データコンストラクタ Zero :: Nat, Succ :: Nat -> Nat に加えて、それぞれ Zero :: Nat, Succ :: Nat -> Nat と云う カインド を持つような 型 Zero, Succ も自動的に定義されるようになったのです。

うーん。どうもわかりませんね……。それの何が嬉しいの……？というところで、そろそろ例の方に戻りましょうか。

返り値問題：型リストで引数の一覧を表現する

百聞は一見にしかず。思い切って実際に使われている定義を見てしまいましょう。次が関数の引数と返り値をエンコードした NAry as a の定義です。as が引数の型の一覧、aが返り値を表します。 

data NAry (as :: [*]) a where
  Value :: a -> NAry '[] a
  Arg   :: (b -> NAry xs a) -> NAry (b ': xs) a

data宣言なのにwhereがついている……？それは、DataKinds 機能拡張の他に、GADTsと云う機能拡張が使われているからです。GADTs を簡単に説明すると、データコンストラクタによって型を柔軟に指定出来る機能です。上の定義を GADTs を使わないで書くと下のようになります。 

data NAry' (as :: [*]) a = (as ~ '[]) => Value' a
                         | forall b xs . (as ~ (b ': xs))
                           => Arg' (b -> NAry' xs a)

Value コンストラクタでは as ‘[] と云う制約が追加されていて、Arg’コンストラクタでは b, xs が全称量化されていて、更に as (b ’: xs) と云う制約が掛かっていますね。b や xs は左辺に登場しないといけないので forall を伴っているわけですが、では後者の制約はどう云う事でしょう？

一般に、a b と云う型制約は「型 a と型 b は等しい」と云う意味です。従って、上の制約 as (b ’: xs) は 

型 `as` と、型 `b ': xs` は等しい

と云う意味になります。何故このような制約を掛けているのでしょうか？それは、型引数 as が右辺のデータコンストラクタの定義に一度も登場しないので、具体的に型を決めてやることが出来なくなるからです。一般に、このように左辺にしか登場しない型引数を持つ型を「幽霊型(Phantom Type)」と呼びます。

分かり易くするために、例えば、上のNAry’から型同値性の制約を抜いて 

data NAry' (as :: [*]) a = Value' a
                         | forall b xs. Arg' (b -> NAry' xs a)

として GHCi で読み込んで実験してみましょう。 

ghci> :t Value "hello"
Value "hello" :: NAry ([] *) [Char]

ghci> :t Arg $ const $ Value "hello"
Arg $ const $ Value "hello" :: NAry ((:) * b ([] *)) [Char]

ghci> :t Value' "hello"
Value' "hello" :: NAry' as [Char]

ghci> :t Arg' $ const $ Value' "hello"
Arg' $ const $ Value' "hello" :: NAry' as [Char]

GADTs を使って定義した NAry の方は型の第一引数 as の"型リスト"の型までしっかりと決まっているのに対して、同値性制約を抜いた NAry’ の方は、as が型変数のまま残されて仕舞っているのがわかると思います。同値性制約を復活させれば、NAryも NAry’も同様の結果を返すようになる筈です。 このように、幽霊型をコンストラクタで指定してやることで、この例では型に引数の情報を持たせてやっている訳です。

それでは、以上を踏まえて型の定義を読み下していきましょう。 

data NAry (as :: [*]) a where

早速昇格型のおでましです！as のカインド宣言をみてください。これは、リスト型 [] をカインドレベルに昇格して、要素のカインドを としたものです。が値を持つ型を表すことを思い出せば、つまり、[*]はとりもなおさず（完全適用形の）型のリストのことです。よって、

NAry は型のリスト as と型 a を引数に取る

と読めます。では、コンストラクタの定義を見ていきましょう。 

Value :: a -> NAry '[] a

これは、引数を適用しきって返り値だけになった状態を表すコンストラクタです。‘[] はお馴染の空リストですので、「引数を取らずにaの値を返す」と云う気持ちが表現されているのが判ると思います。 ところで、[]の前についている ’ は何でしょう？これは、型名とコンストラクタの曖昧性を解決するための印です。リストには、リスト自身を表す 型名 [] と、空リストを表す データコンストラクタ [] があります。これらは同名なので、型名の文脈に [] が現れたときどちらを指すのか曖昧になってしまいます。それをはっきりさせるため、昇格型を表す際には接頭辞として ’ を付けるのです。

haskell Arg :: (b -> NAry xs a) -> NAry (b ‘: xs) a これは、「引数を一つ取る」状態を表すコンストラクタです。これも殆んど良いですね。 ’: はもちろん cons です。型名と被らないし曖昧性は無いと思うんですが、構文解析の都合なのか何なのか、頭に ’ を付けないと怒られます。

どうでしょう？急に型リストやGADTsなどが出て来てびっくりしたかもしれませんが、引数の型を型リストとして型引数に持っておく、と云うアイデアさえ押さえればそんなに難しくないと思います。

一般の関数と NAry の相互変換

さて、引数と返り値の型を明示したNAry型を定義しました。「リストの要素を関数に適用させる」という目的を達成するために、一般の関数とNAryの相互変換を行う関数を定義しましょう。

まずは NAry から関数への変換関数 fromNAry を書いてみましょう。先ずは型から…… 

fromNAry :: NAry as a -> ...?

おおっと。変換後の関数の引数の個数がわからないので、このままではちゃんと型を書くことが出来ません。as は型リストなので、こいつから再帰的に関数の型を復元する方法があればいいんだけど……。

そこで活躍するのが、型族(Type Families)の機能です！型族とは、型レベルの関数を定義する機能です。どんな感じに使われるのかを見れば大体使い方がわかると思いますので、早速見てみましょう！ 

type family (xs :: [*]) :~> a :: *
type instance '[] :~> a = a
type instance (x ': xs) :~> a = x -> xs :~> a

infixr :~>

一行目は型族 (:>) のカインドを宣言している部分と見做すことが出来ます。これは、

引数の型リスト as :: [*] と最終的な返り値の型 a を受け取って、カインド * の型を返す型レベル関数

と読みます。TypeOperators 拡張を使うことで、 : から始まる型を中置演算子として定義することが出来ます。

二三行目は、引数の型リストが空リストだったとき、cons だったときに場合分けして定義しています。空リストだった場合は単にaの型、x : xs の形だった場合は、再帰的に x を取って xs :> a を返す関数の型、として定義しています。 このようにパターンマッチと再帰で定義するのは、普通の関数の定義と殆んど同じですね！

さて。これさえ手に入れば、fromNAryの型は簡単に書けてしまうので、あとは素直に再帰で定義を書くだけです！ 

fromNAry :: NAry xs a -> xs :~> a
fromNAry (Value a) = a
fromNAry (Arg f)   = fromNAry . f

実に簡単ですね！

さて、では次に普通の関数から NAry への変換関数 toNAry を定義してみましょう。

これは、fromNAry の時ほど簡単ではありません。何故かと云うと、最初の方に注意した通り、どこまでを引数として見做すのかを教えてやる必要があるからです。それなら、引数にしたい型リストを最初に渡してやればいいんじゃないの？こんな風に。 

toNAry' :: xs -> (xs :~> a) -> NAry xs a

しかし、これは駄目です！何故か？例えば xs は具体的には ‘[String, Int, FilePath] のような型を指す訳ですが、じゃあ、’[String, Int, FilePath] 型の値って何があります……？ありませんよね！’[String, Int, FilePath] 型のカインドは [*] ですが、型が値を持つのはカインドが * の時だけです！

ではどうすればいいのか？こう云う時に使われる技法がシングルトンと云うものです。 まずは、取り敢えず次の定義を見てください。 

data SList (as :: [*]) where
  SNil  :: SList '[]
  SCons :: a -> SList xs -> SList (a ': xs)

これがこれから使うリストのシングルトンです。このトリックは、SListのデータ構造そのものは生のリストと同じで、かつそのデータ構造と同型な [*] 型をその型引数として保持している、というところです。例を見てみましょう。GHCi で読み込んで型を見てみます3。 

ghci> :t SNil
SNil :: SList []

ghci> :t SCons (undefined :: Int) SNil
SCons (undefined :: Int) SNil :: SList [Int]

ghci> :t SCons (undefined :: String) (SCons (undefined :: Int) SNil)
SCons (undefined :: String) (SCons (undefined :: Int) SNil) :: SList [String, Int]

たしかに、値レベルでのリスト構造と、型レベルでのリスト構造が一致していますね！シングルトンとは、このようにデータコンストラクタと対象となる型の構造を同型にして、そこから型の情報を復元出来るようにしたものです4。

また、これはシングルトンであることを忘れれば、これはリストの各要素の値が異なるヘテロリストとも見ることが出来ます。ややこしいですが、面倒なので、以後この記事ではSListを型リストのシングルトンとヘテロリストの両方の用途に使うことにします。

上のシングルトンを使って toNAry’ を実装してみたのが以下です。 

toNAry' :: SList xs -> (xs :~> a) -> NAry xs a
toNAry' SNil a = Value a
toNAry' (SCons _ ts) f = Arg $ toNAry' ts . f

ここでキモとなるのは、第一引数のシングルトンをパターンマッチしてやることで、それと同型な型レベルでのパターンマッチを行っていることです。シングルトンとは、このように型レベルのパターンマッチを値レベルで行う為の技法なのです。DataKinds と GADTs の合わせ技でこのようなことが可能になる前は、 toNAry の為の型クラスを態々定義して、xsの型ごとにインスタンスを宣言してやる、という何とも面倒な方法を採る必要がありました。

ところで、文脈によっては xs の型は一意に決まってきて推論出来る場合があるので、省略出来ると便利です。そこで、型クラスを用いて次のようなトリックを使います。 

class SingList k where
  slist :: SList k

instance SingList '[] where
  slist = SNil

instance SingList xs => SingList (x ': xs) where
  slist = SCons undefined slist

toNAry :: forall xs a. SingList xs => (xs :~> a) -> NAry xs a
toNAry = toNAry' (slist :: SList xs)

つまり、xsの型が確定している場合はそこから SList を作れるので、それを生成するようの型クラスを作ってやる訳です。場合分けをシングルトンの方に押し付けることが出来るので、DataKinds 以前の型レベルプログラミングのように、関数ごとに型クラスを定義してやるハックは必要なくなる訳です。

ところで、この関数の型が forall xs a. SingList xs => (xs :> a) -> NAry xs a と量化されているのは、関数定義内部で slist :: SList xs として言及する必要があるからです。量化しないで単に SingList xs => (xs :> a) -> NAry xs a と云う型宣言だと、関数定義部で xs型に言及出来ないのです。そこで、GHC の ScopedTypeVariables 拡張を使えば、型変数を陽に量化してやることで定義部で型変数に言及することが出来るようになるのです。

こうして、最初に挙げた問題のうち、 「1. どこまでを引数、どこからを返り値とするか？」と云う問題は無事解決しました！やりましたね！

singletons パッケージ

上で紹介したシングルトンの技法は、型レベルプログラミングでは一般的に用いられる手法です。型からシングルトンを生成する方法も機械的に出来るので、それを自動化したり型ではなく関数を自動的に昇格させてくれたりする singletons パッケージと云うものがあります（実際、この技法を知ったのはこのパッケージの原論文のお陰です）。

現行安定板の 7.4.1 では Template Haskell や カインド多相の機能が不測しているため、残念ながら singletons を使うには GHC HEAD が必要です。7.6以降でそうした先進的な機能が使えるようになった暁には、singletons を使った幸福な型レベルプログラミングが約束されるでしょう……！

値を適用しよう！

それでは、遂にリストの値を NAry に適用しましょう！最初の方で、

  1. リストは同一型しか含まないが、関数の引数は異なる型を取り得る

と云う問題を提示しました。これは何の仮定も置かなければ当然解けないので、以下では三つの仮定について採り上げてみます。

  1. 入力をヘテロリストにする
  2. 引数の型が全部 Read のインスタンスだとする
  3. 引数の型が全部同じだと仮定する

それぞれ順に見ていきましょう。

入力をヘテロリストにする

最初の条件設定からはいきなり外れますが、入力をヘテロリストだと仮定してしまいましょう！面倒なので、長さも同じとしてしまえば、簡単に以下のようにかけてしまいます。 

applyHeteroList :: NAry as a -> SList as -> a
applyHeteroList (Value a) SNil = a
applyHeteroList (Value a) (SCons _ _) = a
applyHeteroList (Arg f)   (SCons s ts)  = applyHeteroList (f s) ts
applyHeteroList (Arg f)   SNil = error "This would never happen"

引数の型リストと渡されているヘテロリストの長さは同じなので、本来なら二行目と最後の行のパターンは必要ありませんが、GHC が incomplete pattern だと云うので書きました。これはとても簡単ですね。

引数の型が全部 Read インスタンスだとする 〜Constraint カインド〜

もし NAry as a の as の要素が全部 Read のインスタンスであれば、適用関数は以下のように書けます。 

applyReadList (Value a) []     = Just a
applyReadList (Arg f)   (x:xs) = applyReadList (f $ read x) xs
applyReadList _         _      = Nothing

ここで、リストの値が足りなかったり、多すぎた場合には Nothing を返す、と云う設計にしました。

ではこの型はどう書けばいいでしょう？素直に書くと、 

applyReadList :: NAry as a -> [String] -> Maybe a

となりそうですが、 as の各要素が Read である、と云う条件が付いていないので、これでコンパイルしようとすると GHC に怒られてしまいます……。

というところで、活躍するのが GHC 7.4.1 の新機能、制約カインド(Constraint Kind)です！

制約カインドは、型制約を表す Constraint と云う新しいカインドを導入することで、より柔軟な制約の表現を可能にする言語拡張です。Constraint カインドは GHC.Exts モジュールでエクスポートされています。

型制約って型なの……？と思われるかもしれませんが、Haskellでは、内部的には型クラスの情報は「辞書」として関数の引数に渡されているので、カインドで扱うことが出来る訳です。多分。

具体的には、以下の形の物が Constraint のカインドを持ちます。

例えば、Read :: * -> Constraint ですし、MonadReader :: * -> (* -> *) -> Constraint、(Show a, (xs ’[String, Int], ?x :: Int, Read a)) :: Constraint です。

これを使うと、型クラスシノニムのようなものも定義出来ます。例えば、ユーザガイド からの引用例として以下のものがあります。 

type Stringy a = (Show a, Read a)

foo :: Stringy a => a -> (String, String -> a)
foo x = (show x, read)

ここで、 Stringy a は 「a は Show と Read 両方のインスタンスである」と云う意味の別名になります。これ以前には、 UndecideableInstances 等を使って 

class Stringy a
instance (Show a, Read a) => Stringy a

などと宣言してやる必要がありましたが、これでかなりすっきり書けます。

閑話休題。これを使うことで、 as の各要素が Readのインスタンスである、と云う制約を表現することが出来ます！ 

type family Readable (as :: [*]) :: Constraint
type instance Readable '[] = ()
type instance Readable (x ': xs) = (Read x, Readable xs)

まず、対象の型リストが空である場合は、特に何の制約も必要がありません。次に、x : xs の形をしていた場合、まず先頭の要素がReadのインスタンスであることを要求して、リストの残り部分については再帰的に Readable を適用してやれば、結局全部の要素がReadであることが云えます。Constraint要素のタプルもまた Constraint であるため、この定義はちゃんと動作するわです！

後で便利なので、制約を Read から任意の制約述語に一般化した型を定義しておきましょう。 

type family   All (cxt :: * -> Constraint) (xs :: [*]) :: Constraint
type instance All cxt '[]        = ()
type instance All cxt (x ': xs)  = (cxt x, All cxt xs)

type Readable as = All Read as

やっていることは先程と変わっていません。では、これを使って先程の applyReadList を完成させましょう！ 

applyReadList :: Readable as => NAry as a -> [String] -> Maybe a
applyReadList (Value a) []     = Just a
applyReadList (Arg f)   (x:xs) = applyReadList (f $ read x) xs
applyReadList _         _      = Nothing

できました！では、早速試してみましょう。 

ghci> applyReadList (toNAry (+) :: NAry '[Int, Int] Int) ["12", "23"]
Just 35

どこまでが引数かを指定してやる必要はありますが、上手く動いてますね！やりました！

引数の型が全部同じだと仮定する

先程の例が出来てしまえば。こちらもかなり簡単です！答えを書いてしましましょう〜。 

applyHomoList :: All ((~) b) as => NAry as a -> [b] -> Maybe a
applyHomoList (Value a) []     = Just a
applyHomoList (Arg f)   (x:xs) = applyHomoList (f x) xs
applyHomoList _         _      = Nothing

型レベルの同値性 は二項演算子のように扱えるので5、このようにして「asの全部の型がbに等しい」と書いてしまえば、瞬殺なわけです！

まとめ

ここまで、GADTs や 型族といった旧来の機能と、GHC 7.4.1 の DataKinds や ConstraintKinds と云った最新の機能を組み合わせることにで、こんなことまで出来るようになるんだぜ！と云うのを見てきました。 上のヘテロリストの例では長さが全く同じものを仮定しましたが、長さが一致していなくてもよい、とするとどうしたらよいか？また、リストが Dynamic のリストだったりしたりしたらどうか？といったことを考えてみるのも面白いのではないでしょうか。

また、ここでは紹介出来ませんでしたが、カインド多相言語拡張も中々に強力です。これは、引数のカインドが多相的であるようなデータ型や型クラス、型族を定義出来るようになる拡張です。これを使うことで、例えば今は別れている Typeable, Typeable1, Typeable2といった型クラスを一つの型クラスで代用することが可能になるのです！

また、先程触れた singletons パッケージも、このカインド多相の機能をふんだんに使っているものとなっています。ただ、7.4.* 系では明示的にカインド変数を宣言出来なかったり、まだまだ機能的には制限されたものになっています。幅を効かせてくるのは、きっと GHC 7.6.1 からとなるので、それまで楽しみに待つことにしましょう。

それでは、このあたりで。 Happy Type Checking!

  1. EmptyDataDecls などが入ってくると、少々間違っていることになりますが、まあ気にしなくていいです。↩︎

  2. 実際には * に加えて、生のデータ（Unboxed Data）であることを表す # カインドがあります。↩︎

  3. 型レベルリストを表示する際、(:) * Int ([] *) などと表示されて見辛いので、見易いようにカインド引数を省略して、さらにコンマ区切りのリストの記法に直しています。↩︎

  4. ここでは、即値のヘテロリストを型リストのシングルトンとして扱っていますが、本当は型の代理となる幽霊型 Proxy a を定義して、 

    data Proxy a = Proxy
data SList (as :: [*]) where
  SNil :: SList '[]
  SCons :: Proxy a -> SList as -> SList (a ': as)

    のように Proxyのリストとして定義したほうが良いです。このままでは、型からシングルトンを逆に生成するときに、undefinedを使う必要があって精神衛生上宜しくありません。また、型レベルリストの各要素がシングルトンを持つ場合、そのシングルトンのリストとして定義したほうがやり易いことが多いです。 じゃあ最初からそうしろよ、と云う話なんですが、ちょっと時間がないので、ヘテロリストとの兼用をするために実装をサボりました。まあ、そんなに手間は掛からない筈ですが……。↩︎

  5. セクションは無理っぽいですが……。↩︎

Comments