是否可以在Haskell中编写此函数？

Question

我正在学习依赖类型:在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中写这样的东西吗？

Answer 1

问题是你需要一个 Haskell 目前缺乏的依赖量词。即该(x : A)(xs : Vec A (suc n)) \xe2\x86\x92 ...部分是不能直接表达的。你也许可以使用单例来编写一些东西，但它会非常丑陋和复杂。

\n\n

我只是定义

\n\n

delete \xe2\x88\xb7 Eq a \xe2\x87\x92 a \xe2\x86\x92 Vec a (S n) \xe2\x86\x92 Maybe (Vec a n)\n

\n\n

并接受它。我还将更改参数的顺序，以便Vec可以提供Applicative,Traversable和其他实例。

\n\n\n\n

事实上，没有。为了定义，delete您只需要提供一个要删除的索引：

\n\n

{-# LANGUAGE GADTs, DataKinds #-}\n\ndata Nat = Z | S Nat\n\ndata Index n where\n  IZ :: Index n\n  IS :: Index n -> Index (S n)\n\ndata Vec n a where\n  Nil  :: Vec Z a\n  (:-) :: a -> Vec n a -> Vec (S n) a\n\ndelete :: Index n -> Vec (S n) a -> Vec n a\ndelete  IZ    (x :-  xs)       = xs\ndelete (IS n) (x :- (y :- xs)) = x :- delete n (y :- xs)\n

\n\n

请注意，这x \xe2\x88\x88 xs只不过是一个类型丰富的索引。

\n\n\n\n

这是单例的解决方案：

\n\n

{-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures, UndecidableInstances, TypeFamilies, RankNTypes, TypeOperators #-}\n\ninfixr 5 :-\n\ndata Nat = Z | S Nat\n\ndata family Sing (x :: a)\n\ndata instance Sing (b :: Bool) where\n  STrue  :: Sing True\n  SFalse :: Sing False\n\ndata instance Sing (n :: Nat) where\n  SZ :: Sing Z\n  SS :: Sing n -> Sing (S n)\n\ntype family (:==) (x :: a) (y :: a) :: Bool\n\nclass SEq a where\n  (===) :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (x :== y)\n\ntype instance Z   :== Z   = True\ntype instance S n :== Z   = False\ntype instance Z   :== S m = False\ntype instance S n :== S m = n :== m\n\ninstance SEq Nat where\n  SZ   === SZ   = STrue\n  SS n === SZ   = SFalse\n  SZ   === SS m = SFalse\n  SS n === SS m = n === m\n\ndata Vec xs a where\n  Nil  :: Vec '[] a\n  (:-) :: Sing x -> Vec xs a -> Vec (x ': xs) a\n\ntype family If b x y where\n  If True  x y = x\n  If False x y = y\n\ntype family Delete x xs where\n  Delete x  '[]      = '[]\n  Delete x (y ': xs) = If (x :== y) xs (y ': Delete x xs)\n\ndelete :: forall (x :: a) xs. SEq a => Sing x -> Vec xs a -> Vec (Delete x xs) a\ndelete x  Nil      = Nil\ndelete x (y :- xs) = case x === y of\n  STrue  -> xs\n  SFalse -> y :- delete x xs\n\ntest :: Vec '[S Z, S (S (S Z)), Z] Nat\ntest = delete (SS (SS SZ)) (SS SZ :- SS (SS (SS SZ)) :- SS (SS SZ) :- SZ :- Nil)\n

\n\n

在这里，我们Vec通过元素列表对 s 进行索引，并将单例存储为向量的元素。我们还定义了SEq一个类型类，其中包含一个接收两个单例并返回它们所提倡的值相等或不相等的证明的方法。接下来，我们定义一个类型族Delete，它与通常的列表类似delete，但在类型级别。最后，在实际中delete，我们进行模式匹配x === y，从而揭示是否x等于y，这使得类型族进行计算。

\n