Play_FunctorLaws

Markdown generated from:
Source idr program: /src/Play/FunctorLaws.idr
Source lhs program: /src/Play/FunctorLaws.lhs

VerifiedFunctor in Idris and Haskell

One can argue that this is not the best example since instances of Functor are mostly auto generated in Haskell. Monad laws would be a better example.
I decided on to play with VerfiedFunctor because it is simpler. The focal point is not what is verified but how easy it is to verify code.

Ref: https://www.schoolofhaskell.com/user/edwardk/snippets/fmap
Note the above reference, checking second functor law is redundant.

Idris code example

{- 
 Proofs for Functor Laws!
 (Redefined from Idris' Interfaces.Verified)
-}

module Play.FunctorLaws 


||| Redefined from Interfaces.Verified with slight name changes 
interface Functor f => VerifiedFunctor (f : Type -> Type) where
  identityLaw : (x : f a) -> map Basics.id x = Basics.id x
  distLaw : (x : f a) ->
        (g : b -> c) -> (h : a -> b) -> map (g . h) x = (map g) . (map h) $ x

VerifiedFunctor Maybe where
  identityLaw Nothing = Refl
  identityLaw (Just _) = Refl

  distLaw Nothing _ _ = Refl
  distLaw (Just _) _ _  = Refl

||| Hurah! Who needs unit tests!
VerifiedFunctor List where
  identityLaw [] = Refl
  identityLaw (x::xs) = let ih = (identityLaw xs) in cong ih

  distLaw [] _ _ = Refl
  distLaw (x::xs) g h  = let ih = (distLaw xs g h) in cong ih

Compared to Haskell

Ref: https://blog.jle.im/entry/verified-instances-in-haskell.html

{-# LANGUAGE TemplateHaskell
      , KindSignatures
      , DataKinds
      , GADTs
      , PolyKinds
      , TypeInType 
      , TypeOperators 
      , TypeFamilies
      , StandaloneDeriving
      , UndecidableInstances 
      , ScopedTypeVariables
      , LambdaCase
#-}
module Play.FunctorLaws where

import Data.Singletons.TH
import Data.Promotion.Prelude.Function
import Data.Type.Equality
import Prelude hiding (Maybe)

Note there is no straightforward way to correlate value level map with type level Map so VerifiedFunctor f does not extend Functor f like it does in Idris.

class VerifiedFunctor 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
    identityLaw
        :: Sing (x :: f a)
        -> Fmap a a IdSym0 x :~: x

distLaw is much less readable than in Idris. I have changed order of args for convenience. Here is the legend that helps reading the scary (((:.$) @@ g) @@ h) x:

• type (~>) a b = TyFun a b -> Type
• type (@@) (a :: k1 ~> k) (b :: k1) = Apply a b :: k
• (:.$) :: (b ~> c) ~> ((a ~> b) ~> (a ~> c))

Symbols and GATD-zied type level functions are needed for type level partial application.
Haskell type families do not allow for partial application.

    {- | fmap f (fmap g x) = fmap (f . g) x -}
    distLaw
        :: 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

Instead of using Data.SingBased.List I am redefining it here for clarity:

$(singletons [d|
  data List a = LNil | LCons a (List a) deriving Show
  infixr 9 `LCons`

  map :: (a -> b) -> List a -> List b
  map f LNil = LNil
  map f (LCons x xs) = LCons (f x) (map f xs)
 |])

instance VerifiedFunctor List where

    type Fmap a b g x = Map g x

    sFmap = sMap

    identityLaw = \case
      SLNil       -> Refl
      SLCons _ xs ->
        case identityLaw xs of
          Refl -> Refl

    distLaw g h = \case
      SLNil -> Refl
      SLCons _ xs ->
        case distLaw g h xs of
          Refl -> Refl

Same for Maybe:

$(singletons [d|
  data Maybe a = Nothing | Just a deriving Show

  maybeMap :: (a -> b) -> Maybe a -> Maybe b
  maybeMap f Nothing = Nothing
  maybeMap f (Just x) = Just (f x)
 |])

instance VerifiedFunctor Maybe where

    type Fmap a b g x = MaybeMap g x

    sFmap = sMaybeMap

    identityLaw = \case
      SNothing       -> Refl
      SJust x        -> Refl

    distLaw g h = \case
      SNothing -> Refl
      SJust x  -> Refl

Conclusions:

Haskell example uses singletons to encode type dependent information, the verification relies on trusting singletons to do proper conversion between value level implementation of map and encoded conversions sMap and Map. Idris simply verifies the actual value level code bits.

In addition, Haskell version is hard to read. Am I proving what I think I am proving? I view this to be error prone for DIY work.

Idris wins. Keeping the value level syntax at type level is huge!