如今,我们使用DataKinds
扩展名:
{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}
-- N is a type, but is also a kind now
-- Zero, Succ Zero, ... are values, but are also type-level values of
-- kind N
data N = Zero | Succ N
-- (We could import Proxy the library, instead)
data Proxy (n :: N) = Proxy
-- Now n is restricted to kind N
class Nat (n :: N) where
toInt :: proxy n -> Int
instance Nat Zero where
toInt _ = 0
instance (Nat n) => Nat (Succ n) where
toInt _ = 1 + toInt (undefined :: Proxy n)
然后我们可以使用toInt (Proxy :: Proxy (Succ Zero))
. 相反,toInt (Proxy :: Proxy (Succ Int))
会根据需要引发一个错误。
就个人而言,我也会用更现代的东西替换代理,例如AllowAmbiguousTypes
,TypeApplications
以删除未使用的参数。
{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables,
AllowAmbiguousTypes, TypeApplications #-}
data N = Zero | Succ N
-- Now n is restricted to kind N
class Nat (n :: N) where
toInt :: Int
instance Nat Zero where
toInt = 0
instance (Nat n) => Nat (Succ n) where
toInt = 1 + toInt @n
将此用作toInt @(Succ Zero)
. toInt @n
语法选择类型类中的n
。它不对应于运行时交换的任何值,仅对应于编译时存在的类型级参数。
使用
type Foo = Succ Int
也可以根据需要出错:
• Expected kind ‘N’, but ‘Int’ has kind ‘*’
• In the first argument of ‘Succ’, namely ‘Int’
In the type ‘Succ Int’
In the type declaration for ‘Foo’