这个函数能否用Haskell编写？

Question

这个函数能否用Haskell编写？

7

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

- Rnhmjoj

1

你可以使用 Either，其中 Left xs 表示未删除任何值的原始向量，而 Right ... 表示已删除 x 的新向量。 - chepner

我不建议使用Haskell来学习依赖类型。Haskell从未被设计为依赖类型语言（尽管他们正在取得显著进展），而像单例这样的技巧只是帮助模拟依赖类型的hack。首先在Agda或Idris等DT语言中学习概念，然后你会发现更容易理解Haskell中的编码。 - Benjamin Hodgson

1

一个人也可以考虑到，为Haskell库函数选择的接口可能是一种非依赖性编程的结果，而且只是为了在这种方式下表现良好。与其移植该接口，一个人不妨再三考虑。至少我不会实现删除，而是会实现反转插入的视图。 - pigworker

@BenjaminHodgson 我知道，我本来想用Agda的，但是在NixOS上设置起来有些问题（它在那里得不到很好的支持），所以我决定坚持使用Haskell并进行一些实验。 - Rnhmjoj

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- effectfully · Accepted Answer

问题在于你需要一个依赖量词，而Haskell目前缺乏这个功能。也就是说，(x : A)(xs : Vec A (suc n)) → ... 这部分无法直接表达。你可能可以使用单例来解决问题，但这会变得非常丑陋和复杂。

我建议只需定义：

delete ∷ Eq a ⇒ a → Vec a (S n) → Maybe (Vec a n)

并且对此感到满意。我还会更改Vec参数的顺序，以使提供应用程序、可遍历和其他实例成为可能。

实际上，不需要。为了定义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仅仅是一个类型丰富的索引。

这里有一个使用singleton的解决方案：

{-# 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，使得类型家族计算。