Re: [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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[Benja Fallenstein]

Hi Yitz,

On Jan 2, 2008 10:34 AM, Yitzchak Gale <[EMAIL PROTECTED]> wrote:
> No, only countably many. 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.

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*.

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. 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).

So I disagree that the function types of Hask should automatically be
taken to be countable. 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.

Best,
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[ajb]

G'day all.

Quoting Yitzchak Gale <[EMAIL PROTECTED]>:


Data types consist only of computable elements. Since there
are only countably many computable functions, every data type
has at most countably many elements. In particular, it is a set.


I still say it "isn't a set" in the same way that a group "isn't a set".
Haskell data types have structure that is respected by Haskell
homomorphisms.  Sets don't.

Cheers,
Andrew Bromage
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[Yitzchak Gale]

I wrote:
>> The classical definition of "general recursive function"
>> refers to functions in Integer -> Integer to begin
>> with, so there can only be countably many values by
>> construction.

Luke Palmer wrote:
> Except that there are uncountably many (2^Aleph_0) functions in
> Integer -> Integer.

No, only countably many. By the type expression Integer -> Integer
we mean all Haskell functions mapping Integers to Integers.
There are only countably many of those.

Of course, you can sometimes use Haskell-like notation
for discussing other mathematical concepts. In that context,
you might mean to include uncomputable functions in
your types. (Hey, there's a fun idea - how would you write
the infinite injury algorithm in Haskell?)

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.

-Yitz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[Luke Palmer]

On Jan 1, 2008 3:43 PM, Yitzchak Gale <[EMAIL PROTECTED]> wrote:
> The classical definition of "general recursive function"
> refers to functions in Integer -> Integer to begin
> with, so there can only be countably many values by
> construction.

Except that there are uncountably many (2^Aleph_0) functions in
Integer -> Integer.  That doesn't change the fact that there are
countably many computable functions, as you guys have been saying.
But I think you need to refer to the LC or Turing machine definition
to get countability.

Luke
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[Yitzchak Gale]

Andrew Bromage wrote:
>> [*] Theoretical nit: It's not technically a "set".
>>
>> Consider the data type:
>>
>>  data Foo = Foo (Foo -> Bool)
>>
>> This declaration states that there's a bijection between the elements of
>> Foo and the elements of 2^Foo, which by Cantor's diagonal theorem cannot
>> be true for any set.  That's because we only allow computable functions,
>> and Foo -> Bool is actually an exponential object in the category Hask.

I wrote:
> Data types consist only of computable elements. Since there
> are only countably many computable functions,

What I meant by that is that there are only countably
many lambdas, and we can define a "computable value"
as a lambda.

The classical definition of "general recursive function"
refers to functions in Integer -> Integer to begin
with, so there can only be countably many values by
construction.

> every data type
> has at most countably many elements. In particular, it is a set.
>
> The least fixed point under these restrictions is not a bijection
> between Foo and 2^Foo. It is only a bijection between Foo and
> the subset of computable 2^Foo.

-Yitz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[Yitzchak Gale]

Andrew Bromage wrote:
> [*] Theoretical nit: It's not technically a "set".
>
> Consider the data type:
>
>  data Foo = Foo (Foo -> Bool)
>
> This declaration states that there's a bijection between the elements of
> Foo and the elements of 2^Foo, which by Cantor's diagonal theorem cannot
> be true for any set.  That's because we only allow computable functions,
> and Foo -> Bool is actually an exponential object in the category Hask.

Data types consist only of computable elements. Since there
are only countably many computable functions, every data type
has at most countably many elements. In particular, it is a set.

The least fixed point under these restrictions is not a bijection
between Foo and 2^Foo. It is only a bijection between Foo and
the subset of computable 2^Foo.

-Yitz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[Benja Fallenstein]

On Dec 31, 2007 7:17 AM,  <[EMAIL PROTECTED]> wrote:
> This declaration states that there's a bijection between the elements of
> Foo and the elements of 2^Foo, which by Cantor's diagonal theorem cannot
> be true for any set.  That's because we only allow computable functions,

Nit the nit: Or (more commonly, I think) all continuous functions.

> and Foo -> Bool is actually an exponential object in the category Hask.

- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[ajb]

G'day all.

Quoting David Menendez <[EMAIL PROTECTED]>:


   data A = B

means that "B" constructs a value of type "A". The "=" acts more like the
"::=" in a BNF grammar.


And, indeed, that was the syntax for it in Miranda.


It is *not* a claim that A equals B, since A is a
type and B is a data constructor.


Wrong.  It _is_ a claim that A equals B.  Or, rather, that the set of
values[*] A is defined as the least-fixpoint solution of the equation
A = B.

Think of this:

data IntList = Nil | Cons Int IntList

This corresponds to an equation:

IntList = { Nil } + { Cons } * Int * IntLIst

where plus denotes union (or disjoint union; either works in this
case) and star denotes Cartesian product.

The least fixpoint of this equation is precisely the set of values[*]
in IntList.


Furthermore, types and data constructors
have disjoint namespaces, hence the common idiom of using the same name for
the type and the constructor when the type has only one constructor.


I think that's the major source of the confusion here, yes.

Cheers,
Andrew Bromage

[*] Theoretical nit: It's not technically a "set".

Consider the data type:

data Foo = Foo (Foo -> Bool)

This declaration states that there's a bijection between the elements of
Foo and the elements of 2^Foo, which by Cantor's diagonal theorem cannot
be true for any set.  That's because we only allow computable functions,
and Foo -> Bool is actually an exponential object in the category Hask.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[David Menendez]

On Dec 30, 2007 9:24 AM, Joost Behrends <[EMAIL PROTECTED]> wrote:

> A similar point: The tutorials teach, that "=" has a similar meaning than
> "=" in
> mathematics. But there is a big difference: it is not reflexive. The
> the right side is the definition of the left. Thus "x=y" has still some
> kind of
> temporality, which mathematics doesn't have. Wadler himself describes
> bunches
> of lazily computed equations as "dataflows" somewhere.
>

The "=" in the data declaration syntax is different from the "=" in value
and type declarations.

   type A = B

means that "A" can be used wherever "B" can be used.

   data A = B

means that "B" constructs a value of type "A". The "=" acts more like the
"::=" in a BNF grammar. It is *not* a claim that A equals B, since A is a
type and B is a data constructor. Furthermore, types and data constructors
have disjoint namespaces, hence the common idiom of using the same name for
the type and the constructor when the type has only one constructor.

There is an alternative syntax for data declarations in recent versions of
GHC. Using it, you would write:

   data A where
   B :: A

This defines a type A, and a constructor B which has type A.

   data ClockTime where   TOD :: Integer -> Integer -> ClockTime

This defines a type ClockTime, and a constructor TOD which takes two
Integers and constructs a ClockTime.

   data Pair :: * -> * -> * where
   Pair :: a -> b -> Pair a b

This defines a type constructor Pair, which takes two types and constructs a
new type, and a constructor, also called Pair, which, for arbitrary types a
and b, takes a value of type a and a value of type b and constructs a value
of type Pair a b.

-- 
Dave Menendez <[EMAIL PROTECTED]>

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[Jake McArthur]

On Dec 30, 2007, at 8:24 AM, Joost Behrends wrote:

For adapting hws (one of the reasons for me to be here, not many  
languages have
a native web server) to Windows i must work on time. In System.Time  
i found


data ClockTime = TOD Integer Integer

2 questions arise here: Does this define "TOD" (which i do not find  
elsewhere)

together with ClockTime also ? And: Why is this not:

data ClockTime Integer Integer = TOD Integer Integer ?

Is it just an abbreviation for the first? Or is there a connection to
ClockTime as an "abstract data type" (a notion, which would have a  
subtle
different meaning than in OOP - since "instance" is such different  
thing

here).


You are right that it defines the TOD constructor. As for you second  
question, I will try to be somewhat formal in my response, so  
hopefully I don't just throw you off more. The quick answer is that  
since we already know the parameters on the right side are Integers,  
we don't need to specify them on the left side.


When you define datatypes, you are essentially defining a type-level  
constructors on the left hand side and (value-level) constructors on  
the right hand side. Just like normal functions, constructors and type  
constructors can be parameterized. Let's deviate for a moment from  
Haskell's notation for data types and approach this from the viewpoint  
of a dependently typed language (a language in which there is little  
separating between the type level and the value level). The data type  
we are defining here is called ClockTime, so its type might be  
represented as


 ClockTime :: *

, where * represents "Kind," the type of types. For completeness, the  
sole constructor we define is called TOD and has type


 TOD :: Integer -> Integer -> ClockTime

. Now, let's say we had tried defining ClockTime with parameters as  
you suggested.


 ClockTime' :: Integer -> Integer -> *

Do you see the problem? In order to use the ClockTime type  
constructor, we would have to use Integer values. This (1) does not  
make much sense in a language like Haskell which doesn't have true  
dependent types, and (2) does not help us in any way with our  
definition of the TOD constructor. We already know by the definition  
of TOD that it takes two Integers and returns a ClockTime. If we used  
this modified definition of ClockTime, we would have to parameterize  
it to specify TOD, maybe like.


 TOD' :: Integer -> Integer -> ClockTime' 2 3

(I chose the 2 and 3 arbitrarily, but these exact values have no  
particular relevance here.) This would not work in Haskell.


However, there are cases where you would want to parameterize a type  
constructor. For example, say we _wanted_ our TOD constructor take two  
values of arbitrary types. If we want the type level to reflect the  
types of these parameters, ClockTime must be parameterized.


 ClockTime'' :: * -> * -> *
 TOD''   :: a -> b -> ClockTime'' a b

In Haskell notation, this would be equivalent to

 data ClockTime'' a b = TOD'' a b

. So, to summarize, the reason that we don't use

 data ClockTime Integer Integer = TOD Integer Integer

is because we don't want to parameterize ClockTime, and even if we  
did, we could not use Integer values like this to do it because  
Haskell is not dependently typed.


- Jake
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Basic question concerning data constructors

[Bulat Ziganshin]

Hello Joost,

Sunday, December 30, 2007, 5:24:59 PM, you wrote:

> data ClockTime = TOD Integer Integer

it declares type with name ClockTime (which you may use on type
signatures, other type declarations and so on) with one constructor
TOD accepting two Integer values. the only way to construct value of
this type is to apply TOD to two Integer expressions (believe it or
not but this declaration automatically defines TOD as function with
the following signature:

TOD :: Integer -> Integer -> ClockTime

f.e.:

seconds2clockTime :: Double -> ClockTime
seconds2clockTime s = TOD (floor(s)) (round(s*1e12)

the only way to deconstruct values of this type is to use TOD
constructor in parser matching, f.e.:

clockTime2seconds :: ClockTime -> Double
clockTime2seconds (TOD s p)  =  fromInteger(s) + fromInteger(p)/1e12




-- 
Best regards,
 Bulatmailto:[EMAIL PROTECTED]

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe