指定类型签名中的有序列表

huangapple go评论51阅读模式
英文:

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

huangapple
  • 本文由 发表于 2023年5月18日 02:18:28
  • 转载请务必保留本文链接:https://go.coder-hub.com/76275109.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定