Jump to content

Talk:Kind (type theory)

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

Data type

[edit]

I don't like the use of data types here because they include function types. Proper types as Pierce uses is a less dubious terminology. Pcap ping 23:29, 19 August 2009 (UTC)[reply]

Haskell list example is really bad

[edit]

because [] is also the empty list which has kind *. Pcap ping 00:48, 20 August 2009 (UTC)[reply]

When [] means the empty list, it's a value, which has type [a], which in its turn has kind *. You can't say the empty list has kind *. ShinNoNoir (talk) 17:07, 24 January 2010 (UTC)[reply]

Notation

[edit]

I have replaced all occurrences \Rightarrow with \rightarrow. I believe it's better to use the original notation instead of substituting it for a different notation that has a meaning in Haskell as well. If a notation was to be changed for purposes of legibility, I would change one that isn't the primary point of discussion. --IncipienceThe (talk) 11:25, 23 July 2012 (UTC)[reply]

Commonality of higher-order type operators

[edit]

In the standard library Phobos of the D language there are things like staticMap:

http://dlang.org/phobos/std_typetuple.html#staticMap

An usage example:

alias staticMap!(Unqual, int, const int, immutable int) T;
static assert(is(T == TypeTuple!(int, int, int)));

Where Unqual is a template that given a type removes from it all its outer modifiers, like const, immutable, pure, nothrow, @safe, shared, ecc.

staticMap has kind:

Where [*] a built-in TypeTuple of D language.

Similar things are not uncommon in D programming and rather easy to implement. In Phobos I count about thirty uses of staticMap, so despite not being very commonly used, I can't agree such things are "very seldom encountered" as stated in the Examples section of this article. — Preceding unsigned comment added by 79.36.205.107 (talk) 01:09, 8 September 2012 (UTC)[reply]

Too Haskell centric

[edit]

The article is too Haskell centric. It says "*" is the kind of types. It also has the Haskellish and mathematically unconventional use of exponentials for binary kinds: maths almost universally uses products.

In Felix, which has an explicit kinding system, I use TYPE. What should be mentioned is that a (top level) kind is a category so that, for example, TYPE * TYPE -> TYPE, applied to a suitable mapping, is a bifunctor. You cannot easily write this is you use "*" for TYPE. The Haskell notation is bad and not suitable for a generic Wikipedia article (although of course the Haskell notation should be specified -- as an example!) Yttrill (talk) 19:16, 10 October 2018 (UTC)[reply]