[Haskell-cafe] Basic question concerning data constructors

[Yitzchak Gale]

Hi Benja,

I wrote:
>> By the type expression Integer -> Integer
>> we mean all Haskell functions mapping Integers to Integers.
>> There are only countably many of those.
> ...
>> But that was not the context in this thread. The category
>> Hask that we often mention in discussions about Haskell
>> the programming language is most certainly a small category.

Benja Fallenstein wrote:
> I don't know. My understanding has been that at least part of the
> benefit of denotational semantics is that you can define what an
> expression means without referring back to the syntactic construction
> or the operational semantics of that expression -- and thus use the
> denotational semantics to check whether the operational semantics are
> "right." But if you start with "all Haskell functions," you already
> have to know what a Haskell function *is*.

Denotational semantics maps expressions in a
language - hence, syntax - into something that
represents their semantics. You can choose
different such mappings to represent different
semantics of the same expressions.

The Haskell Report clearly defines what a Haskell
function is in terms of syntax. So my semantics are
well-defined, and they represent what I understand
when I read a Haskell program.

In fact, these semantics do not really depend on
all aspects of the syntax - only the existence of
certain primitive functions, and certain constructions
such as function definition, pattern matching,
ADTs, etc. The same assumptions are made for any
semantics of Haskell.

Benja Fallenstein wrote:
> I think it should be "allowed" to think of the semantics of Haskell as
> being defined independently of the (relatively operational) notion of
> "computable function," and then define "computable function" to be
> that subset of the functions in the model that you can actually write
> in Haskell.

"Computable function" is not operational - it just means
functions that are lambdas, if you'd like. It just so happens
that, so far, those are the only functions we know how
to compute operationally. Maybe that quantum stuff...

But yes, sure you can do that. That seems to be the approach
in some papers. In particular, the one by Reynolds in which he proves
that Haskell types cannot be represented by sets.

Sounds like strong evidence that those are the wrong
semantics to choose when studying Haskell as a programming
language. Though it is certainly interesting to do so
in a theoretical setting.

> And the only explicit non-syntactic constructions of
> models for Haskell-like languages that I'm familiar with aren't
> countable (they contain all continuous functions, which in the case of
> (Integer -> Integer) comes out to all monotonous functions).

It is not any less syntactic than mine. It only differs in
the semantics assigned to the symbol Integer -> Integer.

> So I disagree that the function types of Hask should automatically be
> taken to be countable.

No, I agree with you. It's not automatic. It depends on
your choice of semantics.

> If you want to assume it for some given
> purpose, sure, fine, but IMO that's an additional assumption, not
> something inherent in the Haskell language.

Agreed.

Thanks,
Yitz