quchen / articles Goto Github PK

Under 'Ugly Warts you have the bullet point:

• Mathematically, all monads are functors, but Haskell does not enforce this hierarchy. [...]

In GHC 7.10, this was added:

class Applicative m => Monad (m :: * -> *) where
   [...]

Thus this is no longer true.

You can see the discussion at http://tunes.org/~nef/logs/haskell/18.04.29 at around time 09:13:30

This aligns with the report: https://www.haskell.org/onlinereport/haskell2010/haskellch3.html (section 3.3 Curried Applications and Lambda Abstractions), where for patterns, it desugars as such:

\ p1 … pn -> e = \x1 … xn -> case (x1, …, xn) of (p1, …, pn) -> e

Example

pattern matching sugar

-- evaluates to 1
let f = \(Just a) b -> a + b in (f undefined) `seq` 1
-- exception Prelude.undefined
let f = \(Just a) -> \b -> a + b in (f undefined) `seq` 1

desugared versions

-- evaluates to 1
let f = \a -> \b -> case (a, b) of (Just x, y) -> x + y in (f undefined) `seq` 1
-- exception Prelude.undefined
let f = \a -> case a of (Just x) -> \b -> x + b in (f undefined) `seq` 1

I'm not sure this qualifies as a frequent thing coming up in #haskell, but it certainly is an oddity.

This is a question about your zipWith article.

In your implementation of splitMiddle, did you use

secondHalf = zipOverflow firstHalf xs

instead of something like

secondHalf = drop (length firstHalf) xs

because the former only enumerates once while the second enumerates twice?

The pointfree article on haskell.org mentions a strange function named swing:

swing :: (((a -> b) -> b) -> c -> d) -> c -> a -> d
swing f c a = f ($ a) c

swing map :: forall a b. [a -> b] -> a -> [b]
swing any :: forall a. [a -> Bool] -> a -> Bool
swing foldr :: forall a b. b -> a -> [a -> b -> b] -> b
swing zipWith :: forall a b c. [a -> b -> c] -> a -> [b] -> [c]
swing find :: forall a. [a -> Bool] -> a -> Maybe (a -> Bool)
...

The type is very close to your moeb function, but it is a bit more general. Indeed, it turns out that moeb can be defined in terms of swing and fix:

swing :: (((a -> b) -> b) -> c -> d) -> c -> a -> d
swing f c a = f ($ a) c

moeb ::  (((a -> b) -> b) -> c -> a) -> c -> a
moeb f x = fix (\go -> f ($ go) x)
moeb f = fix . swing f

loeb = moeb fmap = fix . swing fmap

This realization really brought things together for me:

any :: Foldable t => (a -> Bool) -> t a -> Bool
-- `any` takes a predicate and a collection of things, 
-- and returns whether the predicate succeeds for
-- some value in the collection

swing any :: Foldable t => t (a -> Bool) -> a -> Bool
-- `swing any` instead takes a collection of predicates, 
-- and returns whether any of them succeeded.
-- Informally it moves the `t` from the `a` to the `(a -> Bool)`.

fix . swing any :: Foldable t => t (Bool -> Bool) -> Bool
-- `moeb any` removes the `a` entirely, instead the collection
-- is defined in terms of itself and moeb finds a fixed point.

Maybe upload your brainfuck tutorial on School of Haskell? :-)

An Applicative computation is statically determined in its shape, so it either always or never fails. Depending on previous results would introduce the Monad constraint anyway.

While it is true that shape of an applicative computation cannot depend directly on a result of a previous computation, it can depend on an effect of a previous computation. In many if not all Alternative instances, fall _ = empty seems reasonable, but of course not everything that can fail supports <|>.

[I know very little Haskell, so please make allowances here.]
David you write:
"The important take-away message here, again, is that the following two lines are equivalent: both of them calculate f x, and then make the result available inside the (...) under the name y.

y = f x
(...)

f x $ \y -> (...)"

The issue is with the last line. $ expects a function on the left and a 'value' on the right. So shouldn't this be

\y -> (...) $ f x

or flip the arguments:

aFun x = x+x
y = aFun 2
aFun y -- 8

(£) = flip ($)

aFun 2 £ (\y -> (aFun y)) -- 8

Hope this helps. All the best, Martin

• "wrapp"
• "But can we can fix this!"

This is a question about your zipWith article.

You conclude your article by saying that this is a more efficient implementation of Eq for Polygon.

(==) :: Polygon -> Polygon -> Bool
Polygon p1Edges@(edge1:_) == Polygon p2Edges
  = let p2Edges' = rotateUntil (== edge1) p2Edges
    in p1Edges == p2Edges'

I am not convinced. If the polygons have nothing in common, then I expect rotateUntil executes forever.

Am I correct?

I open this issue for a discussion, I agree it's wrong for representing non-ascii encoding using Char8, but this argument is misleading:

The short answer is 'any time you write Data.ByteString.Char8 in your code, your code is probably wrong

There're a lot of cases, especially when handling a large chunk of String, you know it's ASCII, for example you have a dictionary contains 10,000 words, there's nothing wrong to use Char8. It should be used with caution but not "any time, probably wrong".

In the https://github.com/quchen/articles/blob/master/fbut.md#read section you mentioned Data.Text.readMaybe, which does not exist

'Implement that tape a repeat function for it analogous to Data.List.repeat.' doesn't sound like an actual sentence, and it makes it very hard to understand what the exercise wants from you. My understanding is that you want the reader to implement a Stream of constant values, but I'm not sure exactly.

I am convinced that you don't need to worry about the claim of circularity you mention at the top of the second law article, and I think I can explain why. In your article, you quote the free theorem as:

        f .      g =      p .      q -- (1) Given this ...
=> fmap f . fmap g = fmap p . fmap q -- (2) ... this holds

The Kmett article you mention in the warning, however, gives it as...

The free theorem for fmap :: (a -> b) -> F a -> F b is that given functions f, g, k, and h such that

g . h = k . f

then

$map g . fmap h = fmap k . $map f

where $map is the "natural map" for the type constructor F.

... and then goes on to prove that fmap f = $map f (that is the Lemma 1 there), which leads to the free theorem as you quoted it. Now, I think it is fine to skip this preliminary step in your article, as it would make the discussion more complicated than it needs to be. I am only mentioning it because it is likely that the objection to the proof was raised because of a misunderstanding of that original form of the free theorem.

The whole issue, as I understand it, hinges on that fmap and $map play different roles in the free theorem: fmap is the function you are proving something about, while $map is just part of the free theorem generating machinery. Still, fmap f = $map f, and so whoever complained about the proof probably thought: "Wait a minute -- you are proving a theorem about fmap which machinery that uses fmap. That's circularity!" That, however, would be a misunderstanding: $map does not presuppose that a Functor is involved. Nor, by the way, is using it "a bit hand-wavy", something Edward worries about in the conclusion of his article. $map is perfectly well-defined, albeit implicitly, in section 2 of Theorems for Free!. It is simply what you get when you consider a type polymorphic at a single (covariant) position and restrict the type-defining relation being specified there to a function -- in fact, Wadler even makes an aside about how, for lists, in that case the relation happens to be "the familiar 'map' function". To frame it in another way, the procedure for generating $map for a type is essentially the same thing that GHC does when you use DeriveFunctor: a mechanical procedure, which presupposes nothing other than the "shape" of the type... and which happens to produce fmap thanks to category theoretical reasons.

All things considered, I believe you can safely remove the warning at the top of the article. It would be nice to retain the link to Kmett's article, though, perhaps alongside the other ones at the bottom of the article.

in the article,

  fmap f . fmap g
= fmap id . fmap (f . g) <-- how this one comes?
= id . fmap (f . g)      -- by the first functor law
= fmap (f . g)

the derivation is problematic and therefore it derives a improper conclusion.

also,

This means that any function f of type [a] -> [a] commutes with map

are you sure this one is true?

let g = (2*)
let f = filter (>10)

apparently map g . f /= f. map g.

I think the following proof is invalid:

fmap f . fmap g
= fmap id . fmap (f . g)
= id . fmap (f . g) -- by the first functor law
= fmap (f . g)

The proof comes after a statement of an implication, and the first equation in the proof is the antecedent of the implication. but this proof isn't used implicationally. It should read something more like

if fmap f . fmap g = fmap id . fmap (f . g) then ...

but that obviously doesn't help prove the second law.

Very good proposal!

In "Outline of new code", implementations of <* and *>, use <$> instead of fmap for better readability.

Personally, I would also prefer

m >>= f = join (f <$> m)

over

m >>= f = join (fmap f m)

but that's up to debate.

In your excellent article about how the first functor law implying the second in Haskell, I see where you applied the first functor law and the free theorem, but I don't see where you assumed that none of the types involved were the bottom type.

Do you think you could improve that proof by making the use of this assumption explicit?

Code from here seems to give expected results in both GHC 9.0.1 and GHC 8.10.4.

ghci> let op = undefined
|
ghci> (`op` ()) `seq` ()
()
ghci>

This is a question about your zipWith article.

Is flip essential in

rotateUntil p xs = zipWith
    (flip const)
    xs
    (dropWhile (not . p) (cycle xs))

?

My guess is that this can be simplified to

rotateUntil p xs = zipWith
    const
    (dropWhile (not . p) (cycle xs))
    xs

Am I correct?

Hi @quchen. I am fairly new to Haskell, and stumbled upon your loeb article. I would like to write the function maybeLoeb :: Functor f => f (f a -> a) -> Maybe (f a) that is the same as loeb, but returns None instead of entering an infinite loop when loeb is given bad input. However, I cannot figure out how to catch the infinite loop exception that only seems to occur sometimes (other times, the program just never terminates). Any ideas?

E.g., maybeLoeb [(!! 1),(!! 0)] :: Maybe [Int] would return None.

Thanks!

With an explicit type signature, moeb can be given a more general type

moeb :: ((forall b . (a -> b) -> b) -> c -> a) -> c -> a
moeb f x = go where go = f ($ go) x

e.g. compare moeb (\a -> bimap a a) with/without the explicit rank 3(?) signature - the rank 3 version allows a fixpoint with different parameters.

It would be awesome if the README.md would immediately link to the articles, so one would not have to scroll up to actually read a post.

It appears that the "twice" combinator is inferred by this h-m implementation as...

λf x. f (f x) :: ∀c d. (c → d) → c → d

...rather than the more common (e.g. GHCi)...

\f x -> f (f x) :: (t -> t) -> t -> t
-- or even:
\f -> f . f :: (b -> b) -> b -> b

...is this a known discrepancy/limitation?

I also noticed that applying one last substitution brings the former in line with the latter; i.e.:

λf x. f (f x) :: ∀d. (d → d) → d → d

One very simple way to achieve this lies in showType, by swapping...

case (runInfer . fmap (generalize (Env mempty) . snd) . infer env) expr of

...with...

case (runInfer . fmap (generalize (Env mempty) . uncurry applySubst) . infer env) expr of

...though I'm not sure whether that's correct in the general case. If it is, I'm happy to open a pull request for the change; the test suite seems happy with it.

I feel the section about IO is a bit short there. A frequently brought up topic in #haskell and pretty much anywhere else is that people refer to IO in terms of side effects. I'm not sure how you see this, since there are different definitions of "side effects", but afaiu the purpose of haskell IO is exactly that: having IO without side effects, because... the fact that we "do" IO is represented by the type and that is the effect. It's not hidden, it doesn't happen outside of the type system or without the compiler or developer knowing, so it's simply an effect, not a side effect.

If we don't see it that way, then I don't see any way to call haskell pure anymore. Opinions?

In https://github.com/quchen/articles/blob/master/fbut.md#a-op-is-not-x---a-op-x you claim that “(a op)” and “\x -> a op x” are distinct, and demonstrate it using examples.

It should be noted that according to the Haskell 2010 report, this is wrong - it clearly states that (e op) = \ x -> e op x, where “op is a binary operator, e is an expression, and x is a variable that does not occur free in e.”

If anything, this is an example of GHC deviating from the report.

I wanted to share another approach for looking at fix. See https://stackoverflow.com/a/74170472/402428

It is similar to your approach B in that it factors out recursion. However, it puts some additional emphasis on understanding fixed-points as a limits.

Feel free to reference it from here if you think it is helpful.

Previous version was wrong/misleading

In the https://github.com/quchen/articles/blob/master/loeb-moeb.md article it is written:

The interesting part is that the order of the functions is not necessarily left-to-right. The list elements can be swapped around, as long as the circularity is still resolved (otherwise the function won't terminate):

Can you give a more accurate definition of what this “circularity” means? Ie. what is the exact property that must be satisfied in order to avoid non-termination?

I’m trying to debug an issue in the hnix Haskell package where the function loebM causes an infinite loop. I’d like to understand exactly why this happens in order to print out a helpful error instead of looping indefinitely.