在 haskell 中,我可以使用函数 f 的类型签名指定必须以这种方式对必须排序:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module Main where
import Data.Kind
data Nat = Z | S Nat deriving Show
type One = S Z
type Two = S One
data SNat (n :: Nat) where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
f :: (Gt a b) => (SNat a, SNat b) -> SNat b
f (a,b) = b
-- comparing two types:
type Gt :: Nat -> Nat -> Constraint
type family Gt n m where
Gt Z _ = 'True ~ 'False
Gt _ Z = ()
Gt (S n) (S m) = Gt n m
现在我只能构建有序对:
:t f (SS SZ, SZ)
或者我可以使用 hlist:
type HList :: [Type] -> Type
data HList xs where
HNil :: HList '[]
(:&) :: x -> HList xs -> HList (x : xs)
infixr 5 :&
我可以为 2 个元素做函数:
g2 :: (Gt a b) => HList [SNat a, SNat b]
g2 (a :& b :& HNil) = b
3:
g3 :: (Gt a b, Gt a c, Gt b c) => HList [SNat a, SNat b, SNat c]
g3 (a :& b :& c :& HNil) = c
继续成长为g4,g5的复杂类型签名..
是否可以编写通用函数,在类型签名中为任意长度列表指定“仅订购的数字列表”,例如:
gn :: "Some magic" => [Snat a]
在此之后,所有非有序列表都被类型系统拒绝了。
?
你真的想要单例列表:
-- "proto-SList"
-- also "proto-HList", since HList ~= SList' Identity
data SList' (f :: a -> Type) (xs :: [a]) :: Type where
SNil :: SList' f '[]
SCons :: f x -> SList' f xs -> SList' f (x : xs)
infixr 5 `SCons`
type SListNat = SList' SNat -- a proper "SList" requires having a "Sing" type/data family, that determines the function f from the element type a
然后定义排序,作为一个类型族
[Nat] -> Constraint
,以明显的方式
type family Descending (xs :: [Nat]) :: Constraint where
Descending '[] = ()
Descending '[_] = ()
Descending (x : y : xs) = (Gt x y, Descending (y : xs))
然后你可以定义
g
.
g :: Descending xs => SListNat xs -> ()
g SNil = ()
-- note how recursive structure *must* follow structure of Descending
g (x `SCons` SNil) = ()
g (x `SCons` y `SCons` xs) = g (y `SCons` xs)
correct :: ()
correct = g (SS (SS SZ) `SCons` SS SZ `SCons` SZ `SCons` SNil)
incorrect :: ()
incorrect = g (SZ `SCons` SS (SS SZ) `SCons` SS SZ `SCons` SZ `SCons` SNil)
如果你真的必须使用
HList
,你可以例如在使用SNat
(或相应地修改Descending
)之前剥离所有Descending
s
-- using two type families is *necessary*, the equation StripSNats (SNat x : xs) = x : StripSNats xs does *not* work
-- this kind of weirdness is why you should avoid using HList for this purpose
type family StripSNat (x :: Type) :: Nat where StripSNat (SNat x) = x
type family StripSNats (xs :: [Type]) :: [Nat] where
StripSNats '[] = '[]
StripSNats (x : xs) = StripSNat x : StripSNats xs
g' :: Descending (StripSNats xs) => HList xs -> ()
g' HNil = ()
g' (x :& HNil) = ()
g' (x :& y :& xs) = g' (y :& xs)