如何在 Haskell 中定义类型依赖函数族

Question

这是一个(系列(Haskell问题。我对哈斯克尔相当陌生。

假设我们有一个 4 元组 (a1，a2，a3，a4(。我们如何定义一个函数，kth，给出这个元组中的第 k 个元素？例

kth (1,"A",'b',True) 3 = 'b'

如果 a1、a2、a3、a4 的类型相同，那么它的定义相当简单。例如，如果它们都是整数：

kth :: (Int,Int,Int,Int) -> Int -> Int
kth (a1,a2,a3,a4) 1 = a1
kth (a1,a2,a3,a4) 2 = a2
kth (a1,a2,a3,a4) 3 = a3
kth (a1,a2,a3,a4) 4 = a4

我怀疑为什么这不简单，是因为Haskell必须事先知道类型。在库函数fst和snd中，Haskell知道输出类型是形式上第一个元素的类型，而输出类型是后者的第二个元素的类型。因此，没有歧义。在kth中，输出类型依赖于第二个输入，因此Haskell不能根据语法进行类型检查。

现在，假设我们有第 n 个元组 (a1，a2,...,an(。我们能否定义一族长度函数，以便

lengthTuple :: a -> Int
lengthTuple (a1,a2,...,an) = n

Answer 1

这种问题(依赖类型(在 Haskell 中仍然是一个令人头疼的问题。 Prelude 中的元组不太适合这种任务(也许可行(。 但是对于此类问题，您可以使用具有依赖类型的大小向量。

例： https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell

Answer 2

如果索引必须是Int，则无法实现函数，但如果它是自定义的"单例"索引类型，则可以实现函数。从本质上讲，如果我们想模仿依赖类型，我们最好的选择是将单例传递很多，将类型级值连接到术语级值。

下面是一个例子：

{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-}
{-# OPTIONS -Wall #-}
-- custom index type
data Ix = I1 | I2 | I3 | I4
-- associated singleton type (this could be autogenerated using the singletons library)
data SIx (ix :: Ix) where
SI1 :: SIx 'I1
SI2 :: SIx 'I2
SI3 :: SIx 'I3
SI4 :: SIx 'I4
-- type level function
type family T (ix :: Ix) a1 a2 a3 a4 
type instance T 'I1 a1 _ _ _ = a1
type instance T 'I2 _ a2 _ _ = a2
type instance T 'I3 _ _ a3 _ = a3
type instance T 'I4 _ _ _ a4 = a4
-- our "dependent" tuple selector
choose :: (a1, a2, a3, a4) -> SIx ix -> T ix a1 a2 a3 a4
choose (x1, _, _, _) SI1 = x1
choose (_, x2, _, _) SI2 = x2
choose (_, _, x3, _) SI3 = x3
choose (_, _, _, x4) SI4 = x4

如果需要，我们可以"隐藏"SIx ix的ix参数，并使用存在包装器(作为一种依赖和类型(T ix a1 a2 a3 a4，构建一个给定"某个索引"返回"某个组件"的函数。

如果我们有真正的依赖类型，这将更加方便。尽管如此，这是我们目前为在运行时进行类型擦除而付出的代价。如果有一天Haskell将未擦除的pi a . ...类型添加到我们现在拥有的擦除类型forall a . ...，我们将拥有更多的控制权。

Answer 3

正如一些评论中所建议的那样，简短的回答是，你不应该在Haskell中认真地这样做。 如果你发现自己需要编写可以在不同大小的元组上运行的函数，那么你对Haskell的编程是错误的。

但是，定义像lengthTuple这样的函数的惯用方法是使用具有不同元组大小的显式实例的类型类。 如果这是针对库的，请选择一些上限并写入最大大小的实例。 一个合理的选择可能是 15 元组，因为它也是具有Show实例的最大元组：

> (1,2,3,4,5,6,7,8,9,10,11,12,13,14,15)
(1,2,3,4,5,6,7,8,9,10,11,12,13,14,15)
> (1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16)
<interactive>:72:1: error:
• No instance for (Show ...

因此，lengthTuple的定义如下所示：

class Tuple a where lengthTuple :: a -> Int
instance Tuple (a,b) where lengthTuple _ = 2
instance Tuple (a,b,c) where lengthTuple _ = 3
instance Tuple (a,b,c,d) where lengthTuple _ = 4
...up to 15...

乏味，但非常标准。

值得注意的是，可以使用Data.Data泛型编写没有任何样板的lengthTuple。 这些泛型提供了一种以相当通用的方式折叠代数数据类型结构的方法，您可以使用Const函子在计算字段数时忽略数据类型的实际内容：

import Data.Data
import Data.Functor.Const
lengthTuple :: (Data a) => a -> Int
lengthTuple = getConst . gfoldl ((Const n) _ -> Const (n+1))
(_ -> Const 0)

这工作正常，尽管没有直接的方法将其限制为元组，您可能会发现它对非元组的返回值有些令人惊讶：

> lengthTuple (1,2,3,4)
4
> lengthTuple ""
0
> lengthTuple "what the heck?"
2

写kth要困难得多。 你的直觉是对的。 因为表达式kth tuple n的类型取决于值而不是参数的类型n，所以一个简单的定义是不可能的。 其他答案涵盖了几种方法。