型レベルリテラル - LugendrePublic

型レベルリテラル

GHCは型レベルで数値リテラルと文字列リテラルをサポートしているので，多数の事前定義された型レベル定数に簡単にアクセスできる．数値リテラルはNat種で，文字列リテラルはSymbol種である．この機能はDataKinds言語拡張機能によって有効になる．

この機能のためのリテラルの種と他のすべての低水準操作はモジュールGHC.TypeLitsで定義されている．モジュールはそれらの値レベルの対応物と衝突するいくつかの型レベル演算子を定義することに注意せよ(例えば(+))．これらの演算子を参照するインポートおよびエクスポート宣言には，明示的な名前空間注釈が必要であるインポート/エクスポートの明示的名前空間を参照せよ)．

以下は，低水準関数への安全なインタフェースを提供するために型レベルの数値リテラルを使用する例である．

code: tll1.hs

import GHC.TypeLits

import Data.Word

import Foreign

newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a)

clearPage :: ArrPtr 4096 Word8 -> IO ()

clearPage (ArrPtr p) = ...

以下は，単純なレコード操作をシミュレートするために型レベルの文字列リテラルを使用する例である．

code: tll2.hs

data Label (l :: Symbol) = Get

class Has a l b | a l -> b where

from :: a -> Label l -> b

data Point = Point Int Int deriving Show

instance Has Point "x" Int where from (Point x _) _ = x

instance Has Point "y" Int where from (Point _ y) _ = y

example = from (Point 1 2) (Get :: Label "x")

型レベルリテラルの実行時の値

場合によっては，型レベルのリテラルに関連付けられている値レベルのリテラルにアクセスすると便利である．これは関数natValと symbolValを使って行われる．例えば，

code: tll3.hs

GHC.TypeLits> natVal (Proxy :: Proxy 2)

これらの関数は，インスタンス化された型に応じて異なる結果を返す必要があるため，オーバーロードされている．

code: tll4.hs

natVal :: KnownNat n => proxy n -> Integer

-- instance KnownNat 0

-- instance KnownNat 1

-- instance KnownNat 2

-- ...

どの具体的な型レベルリテラルがプログラムで使用されているかが判明し次第すぐに，GHCは制約を取り除く．これはリテラルに対してのみ機能し，任意の型式には機能しないことに留意せよ．例えば，KnownNat (a + b)という形式の制約は，(KnownNat a, KnownNat b)という形式に単純化されない．代わりに，GHCは，a + bを定数値に単純化できるまで，制約をそのままにする．

実行時の整数値または文字列値を対応する型レベルのリテラルに変換することもできる．もちろん，結果の型リテラルはコンパイル時には不明になるため，存在型に隠されている．整数についてはsomeNatVal，文字列に対してはsomeSymbolValを用いることで，変換を行うことができる．

code: tll5.hs

someNatVal :: Integer -> Maybe SomeNat

SomeNat :: KnownNat n => Proxy n -> SomeNat

文字列に対する操作も同様である．

型レベル自然数を使った計算

GHC 7.8は型レベルの自然数を含む算術式を評価することができる．このような式は，足し算，掛け算，およびべき乗のための型族(+), (*), (^) を使用して構成できる．昇格されたブール値を返す(<=?)や，数を制約として比較する(<=)を用いて数を比較することができる．例えば，

code: tll6.hs

GHC.TypeLits> natVal (Proxy :: Proxy (2 + 3))

現時点では，GHCの算術についての推論はかなり限定的である．他の型関数と同じように，算術型関数を評価して結果を比較するだけである．特に，(+)の可換性や結合性などの，算術に関するより一般的な事実をGHCは知らない．

ただし，少しの「逆の」評価を行うことは可能である．たとえば，以下はGHCに型レベルで任意の対数を計算させる方法である．

code: tll7.hs

lg :: Proxy base -> Proxy (base ^ pow) -> Proxy pow

lg _ _ = Proxy

GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8))