<div dir="ltr">Hello,<br><br><div class="gmail_quote"><div dir="ltr">On Tue, Aug 21, 2018 at 7:06 AM Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu">rae@cs.brynmawr.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
> <br>
> Here are some things to think about, if such a proposal is ever written:<br>
> * in this new terminology `4` is not a type, but it also does not fall in any of the other categories, so what is it?<br>
<br>
It's type-level data.<br>
<br></blockquote><div>Why? it is not introduced by a `data` declaration.</div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> * how about `Eq`?<br>
<br>
It's a "constraint constructor", a generalization of a type class.<br>
<br></blockquote><div>Yes, we could refer to the things that construct types of kind K, as K-constructors, and indeed sometimes people do. This is consistent, for example we could say that `4` is a `Nat` constructor. However, it is also convenient to have the concept of a "type constructor", which ranges over all of these things, independent of what their kind is. And, the question of how they were introduced (through a `data` declaration, a class, as a primitive or in some other way) is often completely irrelevant.</div><div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> * how about a type variable `f`?<br>
<br>
It's a type variable. But this is a great question: should it be something else, perhaps a quantified variable (if `f`'s kind isn't Type)? After all, if we have (f :: Nat), then f wouldn't range over types. Indeed, I think calling an f of non-Type kind something other than a type variable would be an improvement. I don't have a great suggestion of what we should call it, though.<br></blockquote><div> </div><div>I think the current terminology works just fine and we don't need to keep inventing new names.</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> * are type functions really type constructors?<br>
<br>
I'm not sure what this means. Right now, if we have `type family F a`, then F isn't really a type constructor, as we can't ever write a plain F in a Haskell program.<br>
<br></blockquote><div>I was referring to the fact that some type functions meet your definition of a type constructor: when applied to enough arguments they produce something of kind `Type`.</div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> * are we really suggesting that we should start supporting things like `'True` at the value level?<br>
<br>
No. I'm suggesting that `'True` and `True` are just two different ways of referring to the same thing. The former is accepted only in a type-level context.<br></blockquote><div><br></div><div>I think that this is the crux of our misunderstanding: if it is really the same thing, then why does it have different names, and some of them are only available sometimes.</div><div>In what sense does a `type data` declaration introduce a `data` constructor, if this `data` constructor can never be used at the value level (e.g., in a case statement)?</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> <br>
> Anyway, it seems to me that we have gone a little off-course, and these changes are not really about making #106 easier to understand.<br>
<br>
But I think they are, for the reasons I've articulated above. The GitHub trail contains several comments to the effect of "this proposal is simply a change in data constructors' namespace" but the proposal describes the new feature as a change to promotion.<br></blockquote><div><br></div><div>We may be able to implement this proposal as just a change to a data-constructor's namespace (I am not sure, last time I tried to do it, it seemed more complicated than this, but this was a long time ago, and I a much more familiar with how GHC works now). Explaining it that way is not simpler, however, as this discussion has illustrated.</div><div><br></div><div>This is a summary:</div><div> * this proposal does NOT change `data` declarations---they work just like they do at the moment,</div><div> * this proposal does NOT change anything to do with promotion (or whatever we want to call what `DataKinds` does)</div><div> * this proposal DOES introduce a new language construct, `type data`, which looks somewhat like a `data` declaration, but it is not the same (e.g. no records, no strictness, unpacking, constructors can't be the same as the LHS, etc.)</div><div> * the purpose of `type data` is to declare some new type-level constants, that's all.</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br></div></div></div>