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