[Haskell-cafe] "show" for functional types
josef.svenningsson at gmail.com
Wed Apr 5 18:50:00 EDT 2006
On 4/5/06, Robert Dockins <robdockins at fastmail.fm> wrote:
> Hey, if we wanted a private conversation, we'd take it off-list. :-)
> > Do you have any reference to the fact that there is any diagreement
> > about the term? I know it has been used sloppily at times but I think
> > it is pretty well defined. See section 4 of the following paper:
> > http://www.dina.kvl.dk/~sestoft/papers/SondergaardSestoft1990.pdf
> It may be that experts have a well defined notion of what it means,
> but I think that non-experts (ie, most people) have a pretty vague
> idea of exactly what it means.
The wikipedia article was very enlightening on this subject,
especially the disclaimer on the top :-) Thanks!
> > So it's a standard substitutivity property. The only problem here is
> > that Haskell has a pretty hairy denotational semantics and I don't
> > think anyone has spelled it out in detail.
> I think that may be the main problem, at least in this context. We
> can take a nice lovely definition of rt, as above, but its
> meaningless without a good semantic model. So we're forced to
> approximate and hand-wave, which is where the disagreement comes in.
Yes, I know what you mean. In the last few weeks this legacy of
hand-waving has been showing its ugly face on the haskell-prime list
as well. Maybe its time to sit down and define properly what we mean
in certain contexts. It seems we would need more than one semantics to
cover the different ways that reason about Haskell program. Just so
that one can say: "Here I'll be using Fast'n-Loose Reasoning(TM)" or
"This law holds in the Handwaving Semantics(TM)". The point is to be
able to reference these precisely defined approximations and thus
enjoying being both sloppy and precise at the same time.
But it's real work doing this kind of thing. During a graduate course
at Chalmers we started at something like this but it grew pretty hairy
More information about the Haskell-Cafe