Send Beginners mailing list submissions to
beginners@haskell.org
To subscribe or unsubscribe via the World Wide Web, visit
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
beginners-requ...@haskell.org
You can reach the person managing the list at
beginners-ow...@haskell.org
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: Type * and * -> * (Erik Dominikus)
----------------------------------------------------------------------
Message: 1
Date: Sun, 14 Mar 2021 17:41:45 +0700
From: Erik Dominikus <erik.dominiku...@gmail.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Type * and * -> *
Message-ID:
<CAOopUjnaCDnP4HAR3=TbVt55mLLNpqxZQx=45qo3wvfs9kz...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
> There's something fundamental I'm missing.
It is not necessarily true, but useful, to think that:
- A *type is* a set of values.
- A *kind* as a set of types.
- The *kind* * is the set of all types.
- The *kind* * -> * is the set of every function with domain * and codomain
*.
- The *type* T -> U is the set of every function with domain T and codomain
U, if each of T and U is a type (a set of values).
For example:
- The type *Bool* is the set {False, True}.
- The type *Maybe Bool* is the set {Nothing, Just False, Just True}.
- *Maybe* is a function such that Maybe(T) = { Nothing } union { Just t | t
in T }.
- *Maybe* is not a type; *Maybe Bool* is a type.
- *a -> a* is the set { \ x -> x }.
Currying and application can happen at both the value level and the type
level:
- The kind of *Either* is ** -> * -> **.
- The kind of *Either a* is ** -> **, if the kind of *a* is ***.
- The kind of *Either a b* is ***, if the kind of *a* is *** and the kind
of *b* is ***.
- The type of *Just* is *a -> Maybe a*.
- The type of *Just x* is *Maybe a*, if the type of *x* is *a*.
> Why is it giving two separate treatments?
It is to show the various ways one *can*
implement/represent/realize/concretize/encode/model
a mathematical construction in Haskell.
You *can* (do type-level programming in Haskell, use all features of C++,
eat spaghetti with a straw, etc.), but the real question has always been:
*should* you?
> If anyone knows of a really thorough and definitive *and *understandable
treatment of Haskell types, I'd appreciate it.
If you mean Haskell 98, then the Haskell 98 Report [1] (especially Chapter
4) seems "thorough and definitive", but I don't know whether you will find
it "understandable".
If you mean the latest Haskell as implemented by GHC, I don't know.
[1] https://www.haskell.org/onlinereport/
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20210314/d71b22ff/attachment-0001.html>
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 152, Issue 7
*****************************************
