Singletons

haskellのpackage

GPT-4.icon

SingletonsとはHaskellのpackageで、型レベル計算と依存型プログラミングをサポートします。これはHaskellの型システムを拡張し、プログラムの一部が特定の型の値に制約されることを許可する能力を提供します。

このパッケージの中心的なアイデアは「singletons」

型のカテゴリで唯一の値を持つ型を作成する

Singletonsパッケージの主な特徴は以下の通りです：

型レベルと値レベルの両方で機能するように関数を定義する

同じ関数の型レベルと値レベルの両方のバージョンを定義することによって達成される

関数とデータ型の定義から自動的にSingletonsを生成する

型と値の間で一貫性を保ちつつ、型のレベルで計算を行うことが可能になる

依存型関数とパターンマッチングをサポート

関数の出力が入力の特定の値に依存するような関数を表現することができる

コード例

code:hs

import Data.Singletons.TH

$(singletons [d|

data Bool = False | True

deriving (Show, Eq)

not :: Bool -> Bool

not False = True

not True = False

|])

code:hs

-- Define a function that enforces that the input must be 'True at the type level.

requireTrue :: Sing 'True -> ()

requireTrue _ = ()

-- Now we can use our function:

main :: IO ()

main = do

let a = sing @'True -- Inferred type is Sing 'True

b = sing @'False -- Inferred type is Sing 'False

print $ requireTrue a -- This compiles, since a has type Sing 'True

-- print $ requireTrue b -- This will not compile, since b has type Sing 'False

このコードは、型レベルでTrueであることを要求するrequireTrueという関数を定義しています。そして、Sing 'True型とSing 'False型の値をそれぞれaとbに代入しています。そしてrequireTrue関数にこれらの値を渡すと、型がSing 'Trueであるaはコンパイルエラーにならず、Sing 'Falseであるbは型チェックに失敗してコンパイルエラーになることが示されています。