 |
|
|
|
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Sometimes, I really love Haskell.
From the people who gave us such gems as
"A monad is just a monoid in the category of endofunctors, what's the
problem?"
and
"What part of
x : σ ∈ Γ
----------
Γ ⊢ x : σ
Γ ⊢ e0 : τ → τ', Γ ⊢ e1 : τ
-----------------------------
Γ ⊢ e0 e1 : τ'
Γ, x : τ ⊢ e : τ'
--------------------
Γ ⊢ λ x . e : τ → τ'
Γ ⊢ e0 : σ, Γ, x : σ ⊢ e1 : τ
-------------------------------
Γ ⊢ let x = e0 in e1 : τ
Γ ⊢ e : σ', σ' ⊑ σ
--------------------
Γ ⊢ e : σ
Γ ⊢ e : σ, α ∉ free(Γ)
-------------------------
Γ ⊢ e : ∀ α . σ
do you NOT understand?"
today I came across this purified gold dust:
"Every Cofree Comonad over an Alternative Functor yields a Monad."
My mind, she is blown.
(Whether this is wonderful or appalling depends on your perspective...)
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
On 14/05/2013 10:10 PM, Orchid Win7 v1 wrote:
>
> "What part of
>
> x : σ ∈ Γ
> ----------
> Γ ⊢ x : σ
>
>
> Γ ⊢ e0 : τ → τ', Γ ⊢ e1 : τ
> -----------------------------
> Γ ⊢ e0 e1 : τ'
>
>
> Γ, x : τ ⊢ e : τ'
> --------------------
> Γ ⊢ λ x . e : τ → τ'
>
>
> Γ ⊢ e0 : σ, Γ, x : σ ⊢ e1 : τ
> -------------------------------
> Γ ⊢ let x = e0 in e1 : τ
>
>
> Γ ⊢ e : σ', σ' ⊑ σ
> --------------------
> Γ ⊢ e : σ
>
>
> Γ ⊢ e : σ, α ∉ free(Γ)
> -------------------------
> Γ ⊢ e : ∀ α . σ
>
> do you NOT understand?"
Love it.
I want it on a tee-shirt.
--
Regards
Stephen
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
On 14/05/2013 10:26 PM, Stephen wrote:
> Love it.
>
> I want it on a tee-shirt.
Funny you should say that...
http://www.cafepress.co.uk/mf/2498088/what-part-of-types-dont-you-understand_tshirt?shop=skicalc
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
On 15/05/2013 8:38 AM, Orchid Win7 v1 wrote:
> On 14/05/2013 10:26 PM, Stephen wrote:
>> Love it.
>>
>> I want it on a tee-shirt.
>
> Funny you should say that...
>
>
http://www.cafepress.co.uk/mf/2498088/what-part-of-types-dont-you-understand_tshirt?shop=skicalc
>
Thanks A.
Now that you post the link I remember that I’ve seen it before. But I’m
not the sort of person that wears themed tee-shirts. It was more just an
appreciation of your humour. I actually have a tee-shirt with a PovRay
generated image but have never worn it. A couple of years ago as an end
of project lark. I created this image http://i.imgur.com/1cpbX.jpg
We got it printed on tee-shirts and wore them during the “go live” floor
walking exercise.
--
Regards
Stephen
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
> Thanks A.
> Now that you post the link I remember that I’ve seen it before. But I’m
> not the sort of person that wears themed tee-shirts. It was more just an
> appreciation of your humour.
Depending on how you look at it, it's either fantastic that the Haskell
guys are such giant nerds, or it's proof that Haskell is an obscure
curiosity that doesn't live in the Real World.
I of course choose the former. ;-)
> I actually have a tee-shirt with a PovRay
> generated image but have never worn it. A couple of years ago as an end
> of project lark. I created this image http://i.imgur.com/1cpbX.jpg
> We got it printed on tee-shirts and wore them during the “go live” floor
> walking exercise.
I have several T-shirts generated with FractInt. (Remember FractInt?) I
keep promising myself that one of these days I'm going to get around to
building that super fractal generator and start producing new material
for my Zazzle page... but it never seems to happen.
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
> "What part of
>
> x : σ ∈ Γ
> ----------
> Γ ⊢ x : σ
>
>
> Γ ⊢ e0 : τ → τ', Γ ⊢ e1 : τ
> -----------------------------
> Γ ⊢ e0 e1 : τ'
>
>
> Γ, x : τ ⊢ e : τ'
> --------------------
> Γ ⊢ λ x . e : τ → τ'
>
>
> Γ ⊢ e0 : σ, Γ, x : σ ⊢ e1 : τ
> -------------------------------
> Γ ⊢ let x = e0 in e1 : τ
>
>
> Γ ⊢ e : σ', σ' ⊑ σ
> --------------------
> Γ ⊢ e : σ
>
>
> Γ ⊢ e : σ, α ∉ free(Γ)
> -------------------------
> Γ ⊢ e : ∀ α . σ
>
> do you NOT understand?"
...In other news, I'm actually kind of impressed that this even renders
in "plain text". Back in the day, anything that wasn't 7-bit ASCII was
100% guaranteed to never, ever work in any software application except
the one that created it. Unicode support has apparently come a long way!
[With apologies to all the people who can't find a suitable font to
render this stuff...]
I actually asked one time what all the equations above mean. [Or, more
exactly, what language they're written in - but several responders went
all out and exposited the whole thing.] It turns out that what it's
actually saying is fairly trivial - it just *looks* damned complicated.
Pretty much like most mathematics, really.
(Then again, open a book written on a foreign language like Korean, and
it looks complicated too - even though it might just be somebody's
shopping list or similar.)
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
On 15/05/2013 8:31 PM, Orchid Win7 v1 wrote:
>
> Depending on how you look at it, it's either fantastic that the Haskell
> guys are such giant nerds, or it's proof that Haskell is an obscure
> curiosity that doesn't live in the Real World.
>
> I of course choose the former. ;-)
>
And you could say that the Former chose you. (To be their representative
on Earth, that is.)
>
> I have several T-shirts generated with FractInt. (Remember FractInt?)
Now that you mention it, yes.
Because it was a mention in the Fractint help files that Pov-Ray could
use the RAW file output to create a heightfield. And I wanted to do a
fly-through through a plasma fractal heightfield.
One of these days I'll get round to it. * :-(
> I keep promising myself that one of these days I'm going to get around to
> building that super fractal generator and start producing new material
> for my Zazzle page...
> but it never seems to happen.
* See above. ;-)
--
Regards
Stephen
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
