是否有可能在Haskell中编写这个函数？
我正在学习依赖类型：在Haskell中，我定义了规范类型
data Vec ∷ Type → Nat → Type where
Nil ∷ Vec a Z
(:-) ∷ a → Vec a n → Vec a (S n)
并实现了Data.List大部分函数，但是我不知道如何编写，如果可能的话，函数就像
delete ∷ Eq a ⇒ a → Vec a n → Vec a (??)
因为结果的长度是未知的。 我已经在Agda中找到了它，并以此方式实施
delete : {A : Set}{n : Nat}(x : A)(xs : Vec A (suc n)) → x ∈ xs → Vec A n
delete .x (x ∷ xs) hd = xs
delete {A}{zero } _ ._ (tl ())
delete {A}{suc _} y (x ∷ xs) (tl p) = x ∷ delete y xs p
如果我理解正确， delete它的x的约束是xs一个元素，在这种情况下，您只需删除x并从长度中减1。 我可以在Haskell中写这样的东西吗？
问题是你需要一个Haskell目前缺乏的依赖量词。 即(x : A)(xs : Vec A (suc n)) → ...部分不能直接表达。 你可以用单身人士做一些东西，但它会非常难看和复杂。
我只是定义
delete ∷ Eq a ⇒ a → Vec a (S n) → Maybe (Vec a n)
并罚款。 我还会将参数的顺序更改为Vec ，以便可以提供Applicative ， Traversable和其他实例。
其实，没有。 为了定义delete你只需要提供一个索引来删除：
{-# LANGUAGE GADTs, DataKinds #-}
data Nat = Z | S Nat
data Index n where
IZ :: Index n
IS :: Index n -> Index (S n)
data Vec n a where
Nil :: Vec Z a
(:-) :: a -> Vec n a -> Vec (S n) a
delete :: Index n -> Vec (S n) a -> Vec n a
delete IZ (x :- xs) = xs
delete (IS n) (x :- (y :- xs)) = x :- delete n (y :- xs)
请注意， x ∈ xs是一个丰富类型的索引。
这是一个单件解决方案：
{-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures, UndecidableInstances, TypeFamilies, RankNTypes, TypeOperators #-}
infixr 5 :-
data Nat = Z | S Nat
data family Sing (x :: a)
data instance Sing (b :: Bool) where
STrue :: Sing True
SFalse :: Sing False
data instance Sing (n :: Nat) where
SZ :: Sing Z
SS :: Sing n -> Sing (S n)
type family (:==) (x :: a) (y :: a) :: Bool
class SEq a where
(===) :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (x :== y)
type instance Z :== Z = True
type instance S n :== Z = False
type instance Z :== S m = False
type instance S n :== S m = n :== m
instance SEq Nat where
SZ === SZ = STrue
SS n === SZ = SFalse
SZ === SS m = SFalse
SS n === SS m = n === m
data Vec xs a where
Nil :: Vec '[] a
(:-) :: Sing x -> Vec xs a -> Vec (x ': xs) a
type family If b x y where
If True x y = x
If False x y = y
type family Delete x xs where
Delete x '[] = '[]
Delete x (y ': xs) = If (x :== y) xs (y ': Delete x xs)
delete :: forall (x :: a) xs. SEq a => Sing x -> Vec xs a -> Vec (Delete x xs) a
delete x Nil = Nil
delete x (y :- xs) = case x === y of
STrue -> xs
SFalse -> y :- delete x xs
test :: Vec '[S Z, S (S (S Z)), Z] Nat
test = delete (SS (SS SZ)) (SS SZ :- SS (SS (SS SZ)) :- SS (SS SZ) :- SZ :- Nil)
在这里，我们通过元素列表对Vec进行索引，并将单例存储为向量的元素。 我们还定义了SEq ，它是一个类型类，它包含一个接收两个单例的方法，并返回它们提升的值的平等证明或它们的不等式。 接下来我们定义一个类型族Delete ，就像通常的列表delete一样，但是在类型级别。 最后，在实际的delete我们在x === y上匹配模式，从而揭示x是否等于y ，这使得类型族计算。