代码之家 › 专栏 › 技术社区 › Asad Saeeduddin

为什么我找不到任何违反法律的行为?

comonad category-theory haskell

0

Asad Saeeduddin · 技术社区 · 4 年前

在Twitter上,chrispenner提出了一个有趣的问题 comonad instance

data MapF f k a = f a :< Map k (f a)
  deriving (Show, Eq, Functor, Foldable, Traversable)

instance (Ord k, Comonad f) => Comonad (MapF f k)
  where
  extract (d :< _) = extract d

  duplicate :: forall a. MapF f k a -> MapF f k (MapF f k a)
  duplicate (d :< m) = extend (:< m) d :< M.mapWithKey go m
    where
    go :: k -> f a -> f (MapF f k a)
    go k = extend (:< M.delete k m)

我对这个comonad实例有点怀疑,所以我试着用 hedgehog-classes f ;the Identity 科摩纳德:

genMap :: Gen a -> Gen (Map Int a)
genMap g = G.map (R.linear 0 10) ((,) <$> G.int (R.linear 0 10) <*> f g)

genMapF :: (Gen a -> Gen (f a)) -> Gen a -> Gen (MapF f Int a)
genMapF f g = (:<) <$> f g <*> genMap g

genId :: Gen a -> Gen (Identity a)
genId g = Identity <$> g

main :: IO Bool
main = do
  lawsCheck $ comonadLaws $ genMapF genId

    âââ Context âââ
    When testing the Double Duplicate law(â ), for the Comonad typeclass, the following test failed:

    duplicate . duplicate $ x â¡ fmap duplicate . duplicate $ x, where
      x = Identity 0 :< fromList [(0,Identity 0),(1,Identity 0)]


    The reduced test is:
      Identity (Identity (Identity 0 :< fromList [(0,Identity 0),(1,Identity 0)]) :< fromList [(0,Identity (Identity 0 :< fromList [(1,Identity 0)])),(1,Identity (Identity 0 :< fromList [(0,Identity 0)]))]) :< fromList [(0,Identity (Identity (Identity 0 :< fromList [(1,Identity 0)]) :< fromList [(1,Identity (Identity 0 :< fromList [(0,Identity 0)]))])),(1,Identity (Identity (Identity 0 :< fromList [(0,Identity 0)]) :< fromList [(0,Identity (Identity 0 :< fromList [(1,Identity 0)]))]))]
      â¡
      Identity (Identity (Identity 0 :< fromList [(0,Identity 0),(1,Identity 0)]) :< fromList [(0,Identity (Identity 0 :< fromList [(1,Identity 0)])),(1,Identity (Identity 0 :< fromList [(0,Identity 0)]))]) :< fromList [(0,Identity (Identity (Identity 0 :< fromList [(1,Identity 0)]) :< fromList [(1,Identity (Identity 0 :< fromList []))])),(1,Identity (Identity (Identity 0 :< fromList [(0,Identity 0)]) :< fromList [(0,Identity (Identity 0 :< fromList []))]))]

    The law in question:
      (â ) Double Duplicate Law: duplicate . duplicate â¡ fmap duplicate . duplicate

    âââââââââââââââ

不幸的是,这个反例很难解析,即使对于非常简单的输入也是如此。

f级 身份 科摩纳德。而且对于任何 f级 , Map f k a 可以分解成 Compose (Map Identity k a) f

这样我们就可以摆脱 f级 身份 贯穿始终:

data MapF' k a = a ::< Map k a
  deriving (Show, Eq, Functor)

instance Ord k => Comonad (MapF' k)
  where
  extract (a ::< _) = a
  duplicate (d ::< m) = (d ::< m) ::< M.mapWithKey (\k v -> v ::< M.delete k m) m

genMapF' :: Gen a -> Gen (MapF' Int a)
genMapF' g = (::<) <$> g <*> genMap g

main :: IO Bool
main = do
  -- ...
  lawsCheck $ comonadLaws $ genMapF'

    âââ Context âââ
    When testing the Double Duplicate law(â ), for the Comonad typeclass, the following test failed:

    duplicate . duplicate $ x â¡ fmap duplicate . duplicate $ x, where
      x = 0 ::< fromList [(0,0),(1,0)]


    The reduced test is:
      ((0 ::< fromList [(0,0),(1,0)]) ::< fromList [(0,0 ::< fromList [(1,0)]),(1,0 ::< fromList [(0,0)])]) ::< fromList [(0,(0 ::< fromList [(1,0)]) ::< fromList [(1,0 ::< fromList [(0,0)])]),(1,(0 ::< fromList [(0,0)]) ::< fromList [(0,0 ::< fromList [(1,0)])])]
      â¡
      ((0 ::< fromList [(0,0),(1,0)]) ::< fromList [(0,0 ::< fromList [(1,0)]),(1,0 ::< fromList [(0,0)])]) ::< fromList [(0,(0 ::< fromList [(1,0)]) ::< fromList [(1,0 ::< fromList [])]),(1,(0 ::< fromList [(0,0)]) ::< fromList [(0,0 ::< fromList [])])]

    The law in question:
      (â ) Double Duplicate Law: duplicate . duplicate â¡ fmap duplicate . duplicate

    âââââââââââââââ

用一些虚构的语法 show MapF' s、反例更容易理解:

x =
{ _: 0, 0: 0, 1: 0 }

duplicate . duplicate $ x =
{
  _: ...,
  0: {
    _: ...,
    1: {
      _: 0,
      0: 0  # notice the extra field here 
    }
  },
  1: {
    _: ...,
    0: {
      _: 0,
      1: 0 # ditto
    }
  }
}


fmap duplicate . duplicate $ x =
{
  _: ...,
  0: {
    _: ...,
    1: {
      _: 0 # it's not present here
    }
  },
  1: {
    _: ...,
    0: {
      _: 0 # ditto
    }
  }
}

因此,我们可以看到不匹配是由在实现中删除的键引起的 duplicate

instance Ord k => Comonad (MapF' k)
  where
  extract (a ::< _) = a

{-
  -- Old implementation
  duplicate (d ::< m) = (d ::< m) ::< M.mapWithKey (\k v -> v ::< M.delete k m) m
-}

  -- New implementation
  duplicate (d ::< m) = (d ::< m) ::< fmap (::< m) m

令我惊讶的是,它通过了所有测试(包括复制/复制测试):

Comonad: Extend/Extract Identity    â <interactive> passed 100 tests.
Comonad: Extract/Extend    â <interactive> passed 100 tests.
Comonad: Extend/Extend    â <interactive> passed 100 tests.
Comonad: Extract Right Identity    â <interactive> passed 100 tests.
Comonad: Extract Left Identity    â <interactive> passed 100 tests.
Comonad: Cokleisli Associativity    â <interactive> passed 100 tests.
Comonad: Extract/Duplicate Identity    â <interactive> passed 100 tests.
Comonad: Fmap Extract/Duplicate Identity    â <interactive> passed 100 tests.
Comonad: Double Duplication    â <interactive> passed 100 tests.
Comonad: Extend/Fmap . Duplicate Identity    â <interactive> passed 100 tests.
Comonad: Duplicate/Extend id Identity    â <interactive> passed 100 tests.
Comonad: Fmap/Extend Extract    â <interactive> passed 100 tests.
Comonad: Fmap/LiftW Isomorphism    â <interactive> passed 100 tests.

Map fmap 结束,即 Functor . 因此,对于这种类型,一个更合适的名称可能是 NotQuiteCofree :

--   Cofree         f a = a :< f (Cofree f a)
data NotQuiteCofree f a = a :< f a

instance Functor f => Comonad (NotQuiteCofree f)
  where
  duplicate (a :< m) = (a :< m) :< fmap (:< m) m -- Exactly what we had before
  extract (a :< _) = a

f级 s(包括 Map k s) 地址:

genNQC :: (Gen a -> Gen (f a)) -> Gen a -> Gen (NotQuiteCofree f a)
genNQC f g = (:<) <$> g <*> f g

-- NotQuiteCofree Identity ~ Pair
genId :: Gen a -> Gen (Identity a)
genId g = Identity <$> g

-- NotQuiteCofree (Const x) ~ (,) x
genConst :: Gen a -> Gen (Const Int a)
genConst g = Const <$> G.int (R.linear 0 10)

-- NotQuiteCofree [] ~ NonEmpty
genList :: Gen a -> Gen [a]
genList g = G.list (R.linear 0 10) g

-- NotQuiteCofree (Map k) ~ ???
genMap :: Gen a -> Gen (Map Int a)
genMap g = G.map (R.linear 0 10) ((,) <$> (G.int $ R.linear 0 10) <*> g)

main :: IO Bool
main = do
  lawsCheck $ comonadLaws $ genNQC genId
  lawsCheck $ comonadLaws $ genNQC genConst
  lawsCheck $ comonadLaws $ genNQC genList
  lawsCheck $ comonadLaws $ genNQC genMap

事实上 不完全免费 生成 据推测 所有这些函子的有效余元对我来说有点重要。 NotQuiteCofree f a 很明显不是同构的 Cofree f a .

函子 s到 Comonad s必须是唯一的直到唯一同构,因为它定义为附加的右半部分。明显不同于 Cofree f级 为了什么 NotQuiteCofree f 不科摩纳德。

现在是实际问题。事实上,我没有发现任何失败是我编写生成器时的错误造成的,或者是hedgehog类中的错误,或者只是运气不好?如果没有,以及 NotQuiteCofree {Identity | Const x | [] | Map k} 真的是科摩纳德,你能想出其他的吗 f级 不完全免费 不

或者,真的是这样吗 f级 不完全免费

0 回复 | 直到 4 年前

1

4

Reed Mullanix 4 年前

Set ,但我想我们应该可以一概而论。然而,这个证明使用了这样一个事实:我们可以在 套

这是Agda的证据,使用 https://github.com/agda/agda-categories

{-# OPTIONS --without-K --safe #-}

module Categories.Comonad.Morphism where

open import Level
open import Data.Product hiding (_Ã_)

open import Categories.Category.Core

open import Categories.Comonad
open import Categories.Functor renaming (id to Id)
open import Categories.NaturalTransformation hiding (id)
open import Categories.Category.Cartesian
open import Categories.Category.Product
import Categories.Morphism.Reasoning as MR
open import Relation.Binary.PropositionalEquality

module Cofreeish-F {o â e} (ð : Category o â e) (ð-Products : BinaryProducts ð) where
  open BinaryProducts ð-Products hiding (_â_)
  open Category ð
  open MR ð
  open HomReasoning

  Cofreeish : (F : Endofunctor ð) â Endofunctor ð
  Cofreeish F = record
    { Fâ = Î» X â X Ã Fâ X
    ; Fâ = Î» f â â¨ f â Ïâ , Fâ f â Ïâ â©
    ; identity = Î» {A} â unique id-comm (id-comm â â-resp-âË¡ (âº identity)) ; homomorphism = Î» {X} {Y} {Z} {f} {g} â
      unique (pullË¡ projectâ â pullÊ³ projectâ â âº assoc) (pullË¡ projectâ â pullÊ³ projectâ â pullË¡ (âº homomorphism))
    ; F-resp-â = Î» eq â unique (projectâ â â-resp-âË¡ (âº eq)) (projectâ â â-resp-âË¡ (F-resp-â (âº eq)))
    }
    where
      open Functor F

  Strong : (F : Endofunctor ð) â Set (o â â â e)
  Strong F = NaturalTransformation (-Ã- âF (F â Id)) (F âF -Ã-)


open import Categories.Category.Instance.Sets
open import Categories.Category.Monoidal.Instance.Sets

module _ (c : Level) where
  open Cofreeish-F (Sets c) Product.Sets-has-all
  open Category (Sets c)
  open MR (Sets c)
  open BinaryProducts {ð = Sets c} Product.Sets-has-all
  open â¡-Reasoning

  strength : â (F : Endofunctor (Sets c)) â Strong F
  strength F = ntHelper record
    { Î· = Î» X (fa , b) â F.Fâ (_, b) fa
    ; commute = Î» (f , g) {(fa , b)} â trans (sym F.homomorphism) F.homomorphism
    }
    where
      module F = Functor F

  Cofreeish-Comonad : (F : Endofunctor (Sets c)) â Comonad (Sets c)
  Cofreeish-Comonad F = record
    { F = Cofreeish F
    ; Îµ = ntHelper record
      { Î· = Î» X â Ïâ
      ; commute = Î» f â refl
      }
    ; Î´ = ntHelper record
      { Î· = Î» X â â¨ id , F-strength.Î· _ â Î â Ïâ â©
      ; commute = Î» f â congâ _,_ refl (trans (sym F.homomorphism) F.homomorphism)
      }
    ; assoc = Î´-assoc
    ; sym-assoc = sym Î´-assoc
    ; identityË¡ = Îµ-identityË¡
    ; identityÊ³ = Îµ-identityÊ³
    }
    where
      module F = Functor F
      module F-strength = NaturalTransformation (strength F)

      Î´ : â X â X Ã F.Fâ X â (X Ã F.Fâ X) Ã F.Fâ (X Ã F.Fâ X)
      Î´ _ = â¨ id , F-strength.Î· _ â Î â Ïâ â©

      Îµ : â X â X Ã F.Fâ X â X
      Îµ _ = Ïâ

      Î´-assoc : â {X} â Î´ (X Ã F.Fâ X) â Î´ X â â¨ id , F.Fâ (Î´ X) â Ïâ â© â Î´ X
      Î´-assoc {X} {(x , fx)} = congâ _,_ refl (trans (sym F.homomorphism) F.homomorphism)

      Îµ-identityË¡ : â {X} â â¨ Îµ X â Ïâ , F.Fâ (Îµ X) â Ïâ â© â Î´ X â id
      Îµ-identityË¡ {X} {(x , fx)} = congâ _,_ refl (trans (sym F.homomorphism) F.identity)

      Îµ-identityÊ³ : â {X} â Îµ (X Ã F.Fâ X) â Î´ X â id
      Îµ-identityÊ³ {X} {(x , fx)} = refl

2

4

Asad Saeeduddin 4 年前

NotQuiteCofree 明显不同于 Cofree ,所以我们希望至少有一些 f NotQuiteCofree f

不完全免费 是每个函子的余元 f级
不完全免费 不是一个免费的comonad

“生成一个cofree comonad(从任何函子)”是比“生成一个comonad”更严格的要求。