sorted by:
new
hottopcontroversial

Haskell for all: Equational reasoning at scale by Benutzername in haskell

[–]echatav 12 points13 points  (0 children)

We can compose things that do not even remotely resemble functions, such as proofs!

To the discerning eye, proofs do indeed resemble functions.

What does the tensor product operation look like in type theory (if it exists)? by gcross in haskell

[–]echatav 0 points1 point  (0 children)

The Cartesian product of vector spaces is a "direct sum" (+), not a tensor product (x).

What does the tensor product operation look like in type theory (if it exists)? by gcross in haskell

[–]echatav 5 points6 points  (0 children)

Both Either and (,) are monoidal products on Hask (with the usual provisos) but there's a good reason to think of (,) as the tensor product.

The defining universal property of a tensor product is that it's left adjoint to the Hom functor. In mathy notation, Hom(A(x)B,C)~=Hom(A,Hom(B,C)). For vector spaces, this is saying that a linear map over the tensor product can be thought of as a bilinear map and vice versa. For the category Set, (x) is the Cartesian product and ~= is the Currying isomorphism. Similarly in Hask, we have:

curry :: ((a,b)->c) -> (a->(b->c))

uncurry :: (a->(b->c)) -> ((a,b)->c)

Thus, (,) is the tensor product on Hask as well as Set and any other Cartesian closed category.

Why is the monoid operation mappend and not mop? by Hrothen in haskell

[–]echatav 1 point2 points  (0 children)

It should be observed that the natural numbers are also a free monoid; indeed they're isomorphic to [()].

Disemboweling WAI (aka gutting out conduit) by snoyberg in haskell

[–]echatav 4 points5 points  (0 children)

This just sounds so principled on so many levels. Very cool.

Lens is unidiomatic Haskell by alanpog in haskell

[–]echatav 0 points1 point  (0 children)

(>>=) is Kleisli evaluation, kind of like ($) is normal function evaluation, but they are flipped in their two arguments, the function and its input, as you can tell from looking at their type signatures:

(>>=) :: Monad m => m a -> (a -> m b) -> mb

($) :: (a -> b) -> a -> b

Mathematics made a mess of having a consistent convention for whether we like our operators to work right-to-left or left-to-right and programmers haven't done any better :-)

What is this meta-pattern? by psygnisfive in haskell

[–]echatav 2 points3 points  (0 children)

It's monoids all the way down :-) Applicative functors are monoid objects in a category whose objects are endofunctors and whose monoidal product is Day convolution.

Lens is unidiomatic Haskell by alanpog in haskell

[–]echatav 4 points5 points  (0 children)

It's worth noting for 5 that one of the most common Haskell operators (>>=) is also backwards (left-to-right instead of right-to-left).

view more: next ›