From Newsgroup: comp.lang.haskell

Yes, I'm just reading a book by a man who said types are sets
and then goes on to "demonstrate" this using Haskell.

I know nothing about Haskell, but I was mistrustful immediately.

And here's the demo (my demo, not the book's demo):

-- Both types have the exact same "extension" (two Integers)
data Apple = Apple Int Int
data Orange = Orange Int Int

-- A function that only accepts an Apple
checkApple :: Apple -> String
checkApple _ = "This is an Apple"

main :: IO ()
main = do
let myFruit = Orange 1 2

-- The line below causes a COMPILE ERROR.
-- Even though Orange has the same structure as Apple,
-- the names are different, so the types are NOT equal.
putStrLn (checkApple myFruit)

. Both types have the same extension, but different names.
And Haskell does /not/ treat them to be equal.

So I, with no knowledge of Haskell, immediately knew Haskell better
than a man who wrote a book that is partially about Haskell.

This is called "nominal typing" what Haskell does here. A type
essentially is a name, like "Apple" or "Orange". Two different
names - two different types.


--- Synchronet 3.21f-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

ram@zedat.fu-berlin.de (Stefan Ram) writes:

Yes, I'm just reading a book by a man who said types are sets
and then goes on to "demonstrate" this using Haskell.

I know nothing about Haskell, but I was mistrustful immediately.

And here's the demo (my demo, not the book's demo):

-- Both types have the exact same "extension" (two Integers)
data Apple = Apple Int Int
data Orange = Orange Int Int

-- A function that only accepts an Apple
checkApple :: Apple -> String
checkApple _ = "This is an Apple"

main :: IO ()
main = do
let myFruit = Orange 1 2

-- The line below causes a COMPILE ERROR.
-- Even though Orange has the same structure as Apple,
-- the names are different, so the types are NOT equal.
putStrLn (checkApple myFruit)

. Both types have the same extension, but different names.
And Haskell does /not/ treat them to be equal.

I'm curious: what did *his* demo look like? Perhaps he was doing
something with typeclasses?

e.g.:

data Apple a b = Apple a b
data Orange a b = Orange a b

class Fruit a where
checkApple :: a Int Int -> String -- a Bool might be better here, but hey...
checkApple _ = "This is not an apple" -- most fruit aren't apples

instance Fruit Apple where
checkApple _ = "This is an apple" -- apples are apples

instance Fruit Orange where
-- no need to override the default behaviour here

main :: IO ()
main = do
let myFruit = Orange 1 2
putStrLn (checkApple myFruit)
--
Regards,
Jonathan Lamothe
https://jlamothe.net
--- Synchronet 3.21f-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

Jonathan Lamothe <jonathan@jlamothe.net> wrote or quoted:

I'm curious: what did *his* demo look like? Perhaps he was doing
something with typeclasses?

The man who I referred to is Bartosz Milewski who wrote an
excellent book on Category Theory, it's excellent because it
explains the basic workings of Haskell's monads very clearly
in chapter "Kleisli Categories" of part I.

I only have some minor quibbles. One thing is, he writes

|type Writer a = (a, String)
. . .
|The syntax for pairs is minimal: just two items in
|parentheses, separated by a comma.

. However, in Python, the parentheses are not necessary,
as in

|p = a, str

(p now is a pair of the two values of a and of str).
A syntax that adds parentheses to this is not "minimal".
Admittedly, for the empty tuple, in Python, one needs to
use parentheses; it is written as "()".

Another thing is "types are sets". He writes:

|2.3 What Are Types?
|
|The simplest intuition for types is that they are sets of
|values. The type Bool (remember, concrete types start with a
|capital letter in Haskell) is a two-element set of True and
|False. Type Char is a set of all Unicode characters like a or A.
. . .
|When we declare x to be an Integer:
|
|x :: Integer
|
|we are saying that it's an element of the set of integers.
|Integer in Haskell is an infinite set, and it can be used to
|do arbitrary precision arithmetic. There is also a finite-set
|Int that corresponds to machine type, just like the C++ int.

and

|Because of the bottom, you'll see the category of Haskell
|types and functions referred to as Hask rather than Set.
. . .
|From the pragmatic point of view, itrCOs okay to ignore
|non-terminating functions and bottoms, and treat Hask as
|bona fide Set.

. So he says that Haskell types are not exactly sets, but
according to him this is because they have the additional
value "bottom" ("_|_"), otherwise they would be sets as I
understand him.

He does not actually wrote a demo for this interpretation,
he just explained it as quoted above.

Still, Bartosz Milewski's excellent 2017 book "Category
Theory for Programmers" is very much recommended!


--- Synchronet 3.21f-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

ram@zedat.fu-berlin.de (Stefan Ram) writes:

. So he says that Haskell types are not exactly sets, but
according to him this is because they have the additional
value "bottom" ("_|_"), otherwise they would be sets as I
understand him.

He does not actually wrote a demo for this interpretation,
he just explained it as quoted above.

The article "Fast and loose reasoning is morally correct", about typing judgments in the presence of bottom and seq, might be of interest here.

https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf
--- Synchronet 3.21f-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

Paul Rubin <no.email@nospam.invalid> wrote or quoted:

The article "Fast and loose reasoning is morally correct", about typing >judgments in the presence of bottom and seq, might be of interest here.

Yes, I know - because exactly this is what the book said.
I just omitted it for brevity. But here's the full quotation:

|From the pragmatic point of view, itrCOs okay to ignore non-terminating |functions and bottoms, and treat Hask as bona fide Set. 1
. . .
|-----------------------------------
|1 Nils Anders Danielsson, John Hughes, Patrik Jansson,
|Jeremy Gibbons, Fast and Loose Reasoning is Morally Correct.
|This paper provides justification for ignoring bottoms in
|most contexts.
|
Quoted from "Category Theory for Programmers".


--- Synchronet 3.21f-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

On 2026-04-20, Stefan Ram <ram@zedat.fu-berlin.de> wrote:

Still, Bartosz Milewski's excellent 2017 book "Category
Theory for Programmers" is very much recommended!

There is a nice Anki deck available for that book: https://ankiweb.net/shared/info/1871528437
--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

On 19/04/2026 19:51, Stefan Ram wrote:

Yes, I'm just reading a book by a man who said types are sets
and then goes on to "demonstrate" this using Haskell.

I know nothing about Haskell, but I was mistrustful immediately.

And here's the demo (my demo, not the book's demo):

-- Both types have the exact same "extension" (two Integers)
data Apple = Apple Int Int
data Orange = Orange Int Int

Why do you call the two integers the "extension" ? It seems to me
they're not the extension of either type, the constructor is part of the extension too (but not the datatype name).
--
Tristan Wibberley

The message body is Copyright (C) 2026 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

On 20/04/2026 20:32, Stefan Ram wrote:

Paul Rubin <no.email@nospam.invalid> wrote or quoted:

The article "Fast and loose reasoning is morally correct", about typing
judgments in the presence of bottom and seq, might be of interest here.

Yes, I know - because exactly this is what the book said.
I just omitted it for brevity. But here's the full quotation:

|From the pragmatic point of view, itrCOs okay to ...

That doesn't really mean much. Pragmatics is kind of the effect of a
language - what it causes. That is, if you ignore them, you do more stuff.

So from the point of view of doing more stuff, regardless of whether its
what you mean to do, it's okay.
--
Tristan Wibberley

The message body is Copyright (C) 2026 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> wrote or quoted:

On 19/04/2026 19:51, Stefan Ram wrote:

-- Both types have the exact same "extension" (two Integers)
data Apple = Apple Int Int
data Orange = Orange Int Int

Why do you call the two integers the "extension" ?

In set theory, two sets are considered equal if and only if
they contain the same elements, regardless of how they were
defined or named.

This concept is also called "extensional equality", because
a set is defined by the elements to which it /extends/.

Even though Apple and Orange have different names and may have
different conceptual purposes in the mind of the programmer,
both have the same set of possible values (a pair of integers).

As the author of that book claimed that types /are/ sets he must
then accept that set theoretic equality applies to these sets.

In set theory, two sets that both contain all pairs of integers
and nothing else are equal, even if they were introduced using
two different names and two different descriptions.

So when that comment said, "both types have the exact same
'extension'", it meant to remind the reader of the fact that if
the types are deemed to be sets, they should be deemed to be equal.

But Haskell does /not/ deem them to be equal, which shows that
Haskell types are /not/ mathematical sets.


--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

On 12/06/2026 00:05, Stefan Ram wrote:

Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> wrote or quoted:

On 19/04/2026 19:51, Stefan Ram wrote:

-- Both types have the exact same "extension" (two Integers)
data Apple = Apple Int Int
data Orange = Orange Int Int

Why do you call the two integers the "extension" ?

[An answer to a different question was snipped out here leaving
half an answer below]

... Haskell does /not/ deem them to be equal, which shows that
Haskell types are /not/ mathematical sets.

Or they don't have the same elements:

(ctorlabel-Apple, 0, 12) is not in Orange, and
(ctorlabel-Orange, 0, 12) is not in Apple
--
Tristan Wibberley

The message body is Copyright (C) 2026 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> wrote or quoted:

On 12/06/2026 00:05, Stefan Ram wrote:

... Haskell does /not/ deem them to be equal, which shows that
Haskell types are /not/ mathematical sets.

Or they don't have the same elements:
(ctorlabel-Apple, 0, 12) is not in Orange, and
(ctorlabel-Orange, 0, 12) is not in Apple

I'd say that that's the way /nominal types/ are /implemented/
in some Haskell implementations. It seems that such tuplets are
used /internally/ by some Haskell implementations using tuples
starting with a data constructor label identifier.

(ctorlabel-Apple, 0, 12) is an internal compiler symbol,
but it is not part of the Haskell language proper, syntax,
or specification. What you see in the language are then exactly
these types as names (or as tags / labels), not types as sets.


--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.lang.haskell

On 12/06/2026 14:17, Stefan Ram wrote:

(ctorlabel-Apple, 0, 12) is an internal compiler symbol,
but it is not part of the Haskell language proper, syntax,
or specification. What you see in the language are then exactly
these types as names (or as tags / labels), not types as sets.

yes, that's what extensions are in set theory.

In fact, ctor-label isn't even an internal part of a haskell compiler.
It's a prefix I used in a presentation of an object of an informal
system in which I interpreted the Haskell to perceive the extension.
--
Tristan Wibberley

The message body is Copyright (C) 2026 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
--- Synchronet 3.22a-Linux NewsLink 1.2