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