[Haskell-beginners] Type * and * -> *

Galaxy Being borgauf at gmail.com
Tue Mar 16 19:12:06 UTC 2021


This is great stuff. I thank everybody.

On Sun, Mar 14, 2021 at 5:42 AM Erik Dominikus <erik.dominikus71 at gmail.com>
wrote:

> > 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20210316/c611c167/attachment.html>


More information about the Beginners mailing list