7.10. 型水準リテラル

GHCは型水準の数値リテラルと文字列リテラルに対応しており、定義済みの大量の型水準の定数へのアクセスを容易にする。数値リテラルの種はNatであり、文字列リテラルの種はSymbolである。この機能はXDataKinds言語拡張によって有効になる。

これらの種と、この機能の全ての低水準の操作はGHC.TypeLitsモジュールで定義されている。このモジュールが定義する型水準の演算子のいくつかは、それに対応する値水準のもの(たとえば(+))と衝突することに注意せよ。これらの演算子に言及するインポートおよびエクスポート宣言は、明示的な名前空間注釈を必要とする(7.3.27. インポート/エクスポートの際の名前空間の明示を見よ)。

低水準の関数に安全なインタフェースを与えるために型水準の数値リテラルを使う例を示す。

import GHC.TypeLits
import Data.Word
import Foreign

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

clearPage :: ArrPtr 4096 Word8 -> IO ()
clearPage (ArrPtr p) = ...

単純なレコード操作をシミュレートするために型水準の文字列リテラルを使う例を示す。

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")

7.10.1. 型水準リテラルに対応する実行時の値

型水準リテラルに対応する値水準のリテラルを利用できると便利なことがある。これは、関数natValとsymbolValを使って為される。例を挙げる。

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

これらの関数は、どの型に具体化されるかによって異なる値を返す必要があるので、多重定義関数になっている。

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

-- instance KnownNat 0
-- instance KnownNat 1
-- instance KnownNat 2
-- ...

GHCは、プログラムで使われているのがどのリテラルであるか具体的に判明すると、即座にこの制約を解消する。これはリテラルに関してのみ行なわれるのであって、任意の型式に対して行なわれるのでない点に注意。例えば、KnownNat (a + b)という形の制約が、(KnownNat a, KnownNat b)に単純化されることはない。a + bを定数へと単純化できる時が来るまで、GHCは制約をそのままにしておく。

実行時の整数や文字列の値を対応する型水準リテラルに変換することも可能である。もちろん、結果として得られる型リテラルはコンパイル時には不明なので、存在型の中に隠される。この変換は、整数についてはsomeNatVal、文字列についてはsomeSymbolValを使うことで行なえる。

someNatVal :: Integer -> Maybe SomeNat
SomeNat    :: KnownNat n => Proxy n -> SomeNat

文字列についても同様である。

7.10.2. 型水準自然数を使った計算

GHC 7.8は、型水準の自然数についての算術式を評価することができる。こういう式は、(+), (*), (^)の、それぞれ加算、乗算、累乗を表す型族を使うことで構成できる。数値を比較するには、昇格した真偽値を返す(<=?)や、数値を制約として比較する(<=)を使う。例を挙げる。

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

現状では、GHCが行なえる算術についての推論には制限が多い。すなわち、算術型関数を評価し、その結果を比較することができるのみである。特に、算術に関するもっと一般的な事実、例えば(+)の可換性や結合性といったことは知らない。

ただし、評価を少しだけ「反対向きに」行なうことが可能である。例えば、以下のようにすると、GHCに任意の対数を型水準で計算させることができる。

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

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