It seems that Functor definitions in Haskell can be accepted if the type is correct.
This code compiles, but it doesn't satisfy the functor law:
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)
Is is possible for Haskell to check if the functor definition satisfies the functor law?
If Haskell cannot, can Agda/Idris do this?
So, while this question seems Haskell specific at first glance, I think it touches on enough aspects of modern Programming Languages theory and research that there's a good CS-general answer here.
As DW says, it's impossible to automatically verify that an implementation satisfies the Functor laws, by Rice's theorem.
However, strongly-typed languages give you several methods for proving properties of programs, so there are several approaches that work:
Refinement Types. These are a lightweight form of dependent types, where you can refine a type by a predicate that values of that type must satisfy. This lets you model things like the type of non-zero integers. These are implemented in LiquidHaskell, and there's an upcoming accepted paper where they extend techniques like this to verify typeclass laws. This is implemented as a checker on top of Haskell, so you can write normal Haskell code and get all the inference you normally would, but you add annotations that get checked using SMT.
Pseudo-dependent types. Haskell has GADTs, data-kinds, type families, and multi-parameter typeclasses, all of which let you reason about properties of types. The trick is that these tools can't do much to reason about values, so you end up "promoting" your functions to the type level (i.e. writing your functions as type families aka functions on types) and proving about them. With these, you get some inference, but not quite as much as you do when writing normal functions.
In the long run, Dependent Types are coming to Haskell, but probably not in as full a way as you see in Idris or Agda.
Full dependent types. This is what Agda and Idris and Coq get you, and often in those languages, writing proofs that your instances satisfy typeclass laws is required. Types can depend on values, functions can return types, everything is merge. You have the full power of higher-order logic here, so if you can prove it, almost always you can prove it in these systems.
The tradeoff is that the inference in the languages is limited: you need to annotate nearly every function definition with its type, and in general, these languages add a degree of complexity above what Haskell has. And, all the proofs are explicit: you have to write the proof yourself that your programs fulfill your laws. Tactics can help to automate this process, but it ends up generally being rather tedious.
It's possible with this: https://blog.jle.im/entry/verified-instances-in-haskell.html.
We need several extensions and the Singleton library.
And your functor become like this:
{-# LANGUAGE MagicHash, RankNTypes, PolyKinds, GADTs, DataKinds,
FlexibleContexts, FlexibleInstances,
TypeFamilies, TypeOperators, TypeFamilyDependencies,
UndecidableInstances, TypeInType, ConstraintKinds,
ScopedTypeVariables, TypeApplications, AllowAmbiguousTypes,
PatternSynonyms, ViewPatterns #-}
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
From: https://www.zhihu.com/question/65775009/answer/263094330