Haskell is the name of a person who studied logic. His name is Haskell Brooks Curry, an American Mathematician.

During his career, his work on the relationship between logic and the types of programming languages had a profound effect on the development of modern programming languages such as the one now called Haskell.

Most of the programmers may have heard of his name from two sources; one is the programming language Haskell, and the other from the theory about a relationship between Type theory and Logic, called Curry-Howard isomorphism. The programming language Haskell, through its purity, makes the great use of Curry-Howard isomorphism for real world applications.

For example, one could write a 'proof' of Yoneda Lemma in Haskell:


-- Hom(A, B) <-> Nat( Hom_op(A, -), Hom_op(B, -)).

y :: (a -> b) ->  (forall c. (c->a)  -> (c->b) )
y = undefined

y_inv :: (forall c. (c->a) -> (c->b)) -> (a -> b)
y_inv  = undefined

Replacing undefined with proper Haskell terms y_inv . y = id and y . y_inv == id is left as an exercise.

In simpler terms, Curry-Howard isomorphism says that the types correspond to a logical statement, and terms to the proofs of the statement. So, writing the terms for above types is the same thing as proving the Yoneda lemma for the category of Haskell types.

Thanks guys!

Haskellってある人物の名前だったのですね。
無論、SPJも影響されています。