7

首先，我从一些典型的类型级自然数开始。

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Z | S Nat

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

所以我想创建一个表示 n 维网格的数据类型。（在评估元胞自动机中发现的内容的概括是 comonadic。）

data U (n :: Nat) x where
  Point     :: x                           -> U Z     x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

这个想法是类型U num x是 s 的一num维网格的类型x，它“聚焦”在网格中的特定点上。

所以我想把它做成一个comonad，我注意到我可以做这个潜在有用的功能：

ufold :: (x -> U m r) -> U n x -> U (Plus n m) r
ufold f (Point x) = f x
ufold f (Dimension ls mid rs) =
  Dimension (map (ufold f) ls) (ufold f mid) (map (ufold f) rs)

就这个组合器而言，我们现在可以实现一个“维度连接”，将 m 维网格的 n 维网格转换为 (n+m) 维网格。cojoin这在处理将产生网格的结果时会派上用场。

dimJoin :: U n (U m x) -> U (Plus n m) x
dimJoin = ufold id

到目前为止，一切都很好。我还注意到该Functor实例可以用ufold.

instance Functor (U n) where
  fmap f = ufold (\x -> Point (f x))

但是，这会导致类型错误。

Couldn't match type `n' with `Plus n 'Z'

但是如果我们制作一些复制意大利面，那么类型错误就会消失。

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f (Dimension ls mid rs) =
    Dimension (map (fmap f) ls) (fmap f mid) (map (fmap f) rs)

好吧，我讨厌复制意大利面的味道，所以我的问题是这个。我怎样才能告诉类型系统Plus n Z等于n？问题是：您不能对会导致dimJoin产生类似类型错误的类型族实例进行更改。

4

1 回答 1

5

你需要的是一个很好的命题相等类型：

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

data Nat = Z | S Nat

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

data (:=) :: k -> k -> * where
  Refl :: a := a

data Natural (n :: Nat) where
  Zero :: Natural Z
  Suc  :: Natural n -> Natural (S n)

plusZero :: Natural n -> n := (n `Plus` Z)
plusZero Zero = Refl
plusZero (Suc n) | Refl <- plusZero n = Refl

这允许您证明关于您的类型的任意事情，并通过在Refl.

一件烦人的事情是，我的plusZero证明需要对所讨论的自然进行归纳，默认情况下您将无法做到这一点（因为它在运行时不存在）。不过，用于生成Natural见证的类型类会很容易。

对于您的特定情况，另一种选择可能只是在您的类型定义中将参数反转为 plus，以便您Z在左侧获得它并自动减少。确保您的类型尽可能简单通常是一个很好的第一步，但是无论如何，对于更复杂的事情，您通常需要命题相等性。

于 2012-10-19T00:29:08.267 回答