类型族实例证明是否可行？

Question

首先,我从一些典型的类型级自然数字开始.

{-# 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产生类似的类型错误.

Answer 1

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

{-# 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左侧的参数并自动减少.确保你的类型尽可能简单,这通常是一个很好的第一步,但是无论如何你都经常需要命题平等来处理更复杂的事情.