英文:
haskell specifying ordered list in type signature
问题
在Haskell中,你可以使用类型签名来指定函数f的参数对必须按照一定顺序排列。你可以通过以下方式实现:
f :: (Gt a b) => (SNat a, SNat b) -> SNat b
f (a, b) = b
然后,你可以扩展这个思路来创建一个通用函数,以指定类型签名中的“仅包含按顺序排列的数字列表”,类似于以下方式:
gn :: "一些魔法" => [SNat a]
这将拒绝所有未按顺序排列的列表。但是,实际上,Haskell的类型系统不直接支持这种类型级别的操作,因此在类型级别实现此类检查可能会相当复杂,并且需要使用高级的类型级别编程技巧。你可能需要使用依赖类型或其他高级类型系统功能来实现这一目标。
英文:
In haskell I can specify with type signature of function f that pair must be ordered in this way:
{-# 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
Now I can construct only ordered pairs:
:t f (SS SZ, SZ)
Or I can go with hlist:
type HList :: [Type] -> Type
data HList xs where
HNil :: HList '[]
(:&) :: x -> HList xs -> HList (x : xs)
infixr 5 :&
And I can do function for 2 elements:
g2 :: (Gt a b) => HList [SNat a, SNat b]
g2 (a :& b :& HNil) = b
for 3:
g3 :: (Gt a b, Gt a c, Gt b c) => HList [SNat a, SNat b, SNat c]
g3 (a :& b :& c :& HNil) = c
Continue to grow into complex type signatures of g4, g5 ..
Is it possible to write general function that specify in type signature "Only list of numbers that ordered" for arbitary length list, so something like:
gn :: "Some magic" => [Snat a]
After this all non ordered list rejected by type system.
?
答案1
得分: 5
你真的想要单例模式用于列表:
-- "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 = ()
-- 注意递归结构 *必须* 遵循 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
,你可以在使用 Descending
之前剥离所有的 SNat
(或相应地修改 Descending
):
-- 使用两个类型家族是*必要的*,方程 StripSNats (SNat x : xs) = x : StripSNats xs *不起作用*
-- 这种怪异性是为什么你应该避免在这个目的上使用 HList 的原因
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)
希望这能帮助你理解代码!如果你需要进一步的解释或翻译,请告诉我。
英文:
You would really want singletons for lists:
-- "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
Then define sortedness, as a type family [Nat] -> Constraint
, in the obvious way
type family Descending (xs :: [Nat]) :: Constraint where
Descending '[] = ()
Descending '[_] = ()
Descending (x : y : xs) = (Gt x y, Descending (y : xs))
Then you may define 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)
If you really must use HList
, you could e.g. strip off all the SNat
s before using Descending
(or modify Descending
accordingly)
-- 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)
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库,让每个人都能够通过互相帮助和分享经验来进步。
评论