7

我正在查看typeclass的法律，Alt如下所示：

class Functor f => Alt f
  where
  (<!>) :: f a -> f a -> f a

其中一项法律是这样的：

<$> left-distributes over <!>:  f <$> (a <!> b) = (f <$> a) <!> (f <$> b)

更详细地说，这是：

fmap f $ (<!>) a b = (<!>) (fmap f a) (fmap f b)

假设我们 uncurry<!>操作，即我们假设类是这样写的：

class Functor f => Alt f
  where
  alt :: (f a, f a) -> f a

我们可以这样写一个组合器：

mapBoth :: Functor f => (a -> b) -> (f a, f a) -> (f b, f b)
mapBoth f = bimap (fmap f) (fmap f)

这表示type Pair a = (a, a)函子与给定函子的组合f。所以它本身就是函子的态射映射。

有问题的法律现在可以这样写（不改变其含义）：

fmap f . alt = alt . mapBoth f

请注意，就像在法律的原始陈述中一样，mapBoth f它只是适用fmap f于 的两个论点。alt

This is akin to demanding that alt is a natural transformation from the functor (f -, f -) to the functor f -.

However, isn't it actually impossible for a function of alt's type not to be a natural transformation? How would one write a "bad" implementation of alt that that typechecks, but would be rejected by the law?

4

2 回答 2

4

While it isn't the consensus of the other answers and comments, this is not a natural property of "real-world" Haskell.

It is helpful to developers who write non-parametric code to know when they should add constraints to remain compatible with code which takes parametricity for granted.

A badly-behaved example

{-# LANGUAGE GADTs #-}

data Badly a where
  End :: a -> Badly a
  Cons :: a -> Badly b -> Badly a

(<++>) :: Badly a -> Badly b -> Badly a
(End a)    <++> r = Cons a r
(Cons a l) <++> r = Cons a (l <++> r)

instance Functor Badly where
  fmap f (End a) = End (f a)
  fmap f (Cons a r) = Cons (f a) r

instance Alt f where
  (<!>) = (<++>)
于 2020-02-24T22:27:13.470 回答
3

Yes the law holds for free, by parametricity.

Even then, these laws still have value.

  1. It allows people to be aware of them without being adepts of programming language theory.

  2. You will want to have these laws around if you port these interfaces to languages with weaker type systems.

  3. Until Haskell is actually given formal semantics, we technically don't know that those free theorems hold. By sufficiently high standards of formality, it's not enough to pretend that Haskell is a pure polymorphic lambda-calculus. So we might as well add and check these "free" laws just in case.

于 2020-02-24T22:04:11.883 回答