2

为模糊的标题道歉，这里有一些上下文：http ://themonadreader.files.wordpress.com/2013/08/issue221.pdf

上一期的 GADTs 文章介绍了 Nat 类型和 NatSing 类型，用于各种类型级别的列表函数（concat、!!、head、repeat 等）。对于其中一些函数，有必要创建类型族以在 Nat 类型上定义 + 和 <。

data Nat = Zero | Succ Nat

data NatSing (n :: Nat) where
    ZeroSing :: NatSing Zero
    SuccSing :: NatSing n -> NatSing (Succ n)

data List (n :: Nat) a where
    Nil  :: List n a
    Cons :: a -> List n a -> List (Succ n) a

无论如何，为了方便调用者，我编写了一个函数“list”，它将普通[a]转换为 。List n a这需要列表的长度作为输入，就像repeat（来自链接的文章）：

list :: [a] -> NatSing n -> List n a
list []      ZeroSing    = Nil
list (x:xs) (SuccSing n) = Cons x (list xs n)
list _       _           = error "length mismatch"

使用辅助函数会很好toNatSing :: Int -> NatSing n，所以上面可以写成

list :: [a] -> List n a
list xs = list' xs (toNatSing $ length xs)
  where
    list' :: [a] -> NatSing n -> List n a
    list' = ... -- same as before, but this time I simply "know" the function is no longer partial

是否可以编写这样的函数toNatSing？我一直在与类型搏斗，但还没有想出任何东西。

非常感谢！

4

3 回答 3

6

不，你不能写这样的函数。

类型函数

Int -> NatSing n

说它可以将任何整数转换为多态 NatSing。但是没有多态性NatSing。

您在这里似乎想要的是n由传入的Int. 那将是一个依赖类型：

(n :: Int) -> NatSing n

这样的事情在 Haskell 中是不可能的。您必须使用 Agda 或 Idris 或其他依赖类型的语言。单例破解正是 Haskell 解决此问题的方法。如果要根据值进行区分，则必须将值提升到类型级别，这就是NatSing。

您可以编写一个返回 a NatSingfor some n的函数，方法是将其包装n在一个存在类型中：

data ExNatSing where
  ExNatSing :: NatSing n -> ExNatSing

但这在实践中不会给您带来太多好处。通过n总结，您会丢失有关它的所有信息，并且以后无法根据它做出决定。

通过完全相同的参数，你也可以不希望定义一个函数

list :: [a] -> List n a

您可以用来节省一些打字工作的唯一方法是定义一个NatSing自动构造值的类型类：

class CNatSing (n :: Nat) where
  natSing :: NatSing n

instance CNatSing Zero where
  natSing = ZeroSing

instance CNatSing n => CNatSing (Succ n) where
  natSing = SuccSing natSing

然后，你可以说：

list :: CNatSing n => [a] -> List n a
list xs = list' xs natSing
  where
    list' :: [a] -> NatSing n -> List n a
    list' = ... -- same as before, but still partial

在这里，您使用 this 的类型上下文使 GHC 填充正确的NatSing. 然而，这个函数仍然是部分的，因为函数的调用者仍然可以选择n使用什么。如果我想使用 a[Int]的长度3作为 aList (Succ Zero) Int它会崩溃。

同样，您可以将其包装在存在主义中：

data SomeList a where
  SomeList :: NatSing n -> List n a -> SomeList a

然后你可以写

list :: [a] -> SomeList a
list []       = SomeList ZeroSing Nil
list (x : xs) = case list xs of
                  SomeList n xs -> SomeList (SuccSing n) (x : xs')

同样，好处很小，但与 相比ExNatSing，至少有一个好处：您现在可以暂时解开 aSomeList并将其传递给在 a 上操作的函数List n a，获得类型系统保证列表的长度如何被这些转换功能。

于 2013-11-06T00:05:01.660 回答
2

你想要的看起来像 (Int -> (exists n . NatSing n))，其中n提前未知。你可以用类似（未经测试）的东西来做到这一点：

data AnyNatSing where
  AnyNatSing :: NatSing n -> AnyNatSing

toNatSing :: Int -> AnyNatSing
toNatSing n
  | n > 0 = case toNatSing (n - 1) of
      AnyNatSing n -> AnyNatSing (SuccSing n)
  | otherwise = AnyNatSing ZeroSing
于 2013-11-05T23:48:36.540 回答
1

正如 Louis Wassermann 所说，与您想要的最接近的是存在主义包装器，它NatSing从外部变成单态。

不过我认为这没什么用，因为它基本上只是抛弃了长度的类型检查，而你只剩下一个愚蠢的标准整数类型。有更简单的方法，例如，使用愚蠢的标准整数类型和普通的 Haskell 列表......

但是有一种选择可能不是那么无用。x请记住，如果您从函数返回一些值，或者传递一个高阶并用;调用它，这几乎是等效的。x我认为 lisps 特别喜欢这种持续传递技巧。

对于您的示例，您需要一个能够接受任何长度类型的列表的函数。嗯，这样的函数当然存在，例如，一个标量积需要两个长度相等的列表，但不关心长度是多少。然后它返回一个简单的单态数。为简单起见，让我们考虑一个更简单sum的列表类型：

sumSing :: Num a => List (n::Nat) a -> a
sumSing Nil = 0
sumSing (Cons x ls) = x + sumSing ls

然后你可以这样做：

{-# LANGUAGE RankNTypes     #-}

onList :: (forall n . CNatSing n => List n a -> b) -> [a] -> b
f`onList`l = f (list l)

（list具有CNatSing类约束的 kosmicus 变体）并将其称为

sumSing `onList` [1,2,3]

...当然，它本身并没有比存在主义解决方案更有用（我认为，它实际上对类似于这种RankN东西的东西脱糖）。但是你可以在这里做更多的事情，比如标量积示例——提供两个列表并通过类型系统实际上确保它们具有相同的长度。这对于存在主义来说会更丑陋：你基本上需要一个单独的TwoEqualLenLists类型。

于 2013-11-06T00:43:47.137 回答