This is great stuff. I thank everybody.
On Sun, Mar 14, 2021 at 5:42 AM Erik Dominikus
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/ _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners