在 Haskell 等語言中是否無法表示 Functor 等的公理？

01-08

Haskell 中定義的 Functor 似乎只要類型正確就可以，無從保證確實是一個 functor。比如：
data Bst a = NIL | Node a (Bst a) (Bst a) deriving (Eq, Ord, Show)
instance Functor Bst where fmap _ NIL = NIL fmap f (Node v left right) = Node (f v) (fmap f right) (fmap f right)
這樣的代碼也能通過，但這明顯不對，不符合 fmap id = id
import Test.Hspec
bstOfNums = Node (1::Integer) (Node (3::Integer) NIL NIL) (Node (5::Integer) NIL NIL)
main :: IO () main = hspec $ do describe "fmap" $ do it "shoud map id to id" $ fmap id bstOfNums `shouldBe` bstOfNums
報錯：

1) fmap shoud map id to id expected: Node 1 (Node 3 NIL NIL) (Node 5 NIL NIL) but got: Node 1 (Node 5 NIL NIL) (Node 5 NIL NIL)
當然，要求 Haskell 表達這種公理也許不現實，那麼諸如 Agda, Idris 這種 dependent type 的語言能不能表達呢？

idris可以通過證明來保證law。

不合法的實現過不了編譯。

%default total


interface MyFunctor (f: Type -&> Type) where

    map : (func: a -&> b) -&> f a -&> f b

    law1 : (x: f a) -&> map Prelude.Basics.id x = x

    law2 : (x: f a) -&> (g: b -&> c) -&> (h: a -&> b)

        -&> map g (map h x) = map (g . h) x
data BST : Type -&> Type where

    Nil : BST a

    Node : (c: a) -&> (l: BST a) -&> (r: BST a) -&> BST a
implementation MyFunctor BST where

    map _ Nil          = Nil

    map g (Node v l r) = Node (g v) (map g l) (map g r)
    law1 Nil          = Refl

    law1 (Node v l r) = rewrite law1 l in

                            rewrite law1 r in

                                Refl

law2 Nil _ _ = Refl law2 (Node v l r) g h = rewrite law2 l g h in rewrite law2 r g h in Refl

不開擴展不行，連（命題層面的）等號都表示不出來

所以我站 idris：https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Interfaces/Verified.idr

第一個就是 VerifiedFunctor

Verify your Typeclass Instances in Haskell Today!

藉助各種擴展以及Singleton庫是可以做得到的。畢竟有Curry-Howard isomorphism，類型即命題，程序即證明。然後你會發現你的Functor變成了：

class Functor f where type Fmap a b (g :: a ~&> b) (x :: f a) :: f b


    sFmap

        :: Sing (g            :: a ~&> b)

        -&> Sing (x            :: f a   )

        -&> Sing (Fmap a b g x :: f b   )
    -- | fmap id x == x

    fmapId

        :: Sing (x :: f a)

        -&> Fmap a a IdSym0 x :~: x

-- | fmap f (fmap g x) = fmap (f . g) x fmapCompose :: Sing (g :: b ~&> c) -&> Sing (h :: a ~&> b) -&> Sing (x :: f a ) -&> Fmap b c g (Fmap a b h x) :~: Fmap a c (((:.$) @@ g) @@ h) x

畢竟有柯里-霍華德同構，想用類型表示公設總能表示出來的：

{-# OPTIONS -XTypeOperators -XKindSignatures #-} import Proof.Equational

class Functor f =&> FunctorLaws f where fmap_id :: fmap id (x :: f a) :=: x fmap_compose :: gh y :=: g (h y) -&> fmap gh (x :: f a) :=: fmap g ((fmap h) x)

至於怎麼證明則是另一個故事。

說到證明，當然就會想到Coq了。coq-ext-lib 有定義函子，也定義了函子公設。如果不想出具證明的話（真的不願意證嗎？）還可以用 QuickChick 來進行隨機測試。

你代碼改成

data Bst a = NIL | Node a (Bst a) (Bst a) deriving (Eq, Ord, Show)

instance Functor Bst where fmap _ NIL = NIL fmap f (Node v left right) = Node (f v) (fmap f left) (fmap f right)

就應該能通過了。。