haskell在类型签名中指定有序列表

Question

在 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 :&

我可以为两个元素执行函数：

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]

此后，所有非有序列表都被类型系统拒绝。

？

Answer 1

你真的想要列表的单例：

-- "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删除所有s （或进行相应修改）SNatDescendingDescending

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