Gregg Reynolds dev at mobileink.com
Tue Feb 16 12:34:28 EST 2010

```On Sat, Jan 30, 2010 at 1:24 AM, Conal Elliott <conal at conal.net> wrote:

> I call it "an m" or (more specifically) "an Int m" or "a list of Int".  For
> instance, "a list" or "an Int list" or "a list of Int".  - Conal
>
>
> On Wed, Jan 27, 2010 at 12:14 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
>
>> On Wed, Jan 27, 2010 at 11:39 AM, Jochem Berndsen <jochem at functor.nl>
>> wrote:
>> >> Now, here's the question: Is is correct to say that [3, 5, 8] is a
>> >
>> > In what sense would this be a monad? I don't quite get your question.
>>
>> I think the question is this:  if m is a monad, then what do you call
>> a thing of type m Int, or m Whatever.
>>
>> Luke
>>
>
Conal's is the most sensible approach - "what do you call it" amounts to
"what sort of a thing is it", and the best we can say in that respect is
"er, its a thing of type m Whatever".  (My preference, if maximal
explicitness is needed, is to say "it's a token of its type"; some say "term
of type m Whatever".)  Trying to classify such a thing as "value", "object",
"computation", "reduction" etc. inevitably (and necessarily) leads to
tail-chasing since those notions are all essentially equivalent.  Plus they
miss the essential point, which is the typing.

Original poster would probably find Martin-Lof's philosophically-tinged
writings very good on this - clear, reasonably simple, and revelatory, if
you've never closely looked at intuitionistic logic before.  Truth of a
proposition, evidence of a judgment, validity of a
On
the meanings of the Logical Constants and the Justifications of the Logical
Laws <http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.html>.
Presents a completely new (to me) way of thinking about "what is it,