Type level programming consistency

[razcore-rad]

Context

1. Indicate the affected section (i.e. top-level folder)
   Syntax

2. Indicate what kind of issue this is
   Bug

3. If it applies, indicate the file to which you are referring using non-numerical-ordering names

• Syntax/Type-Level-Programming-Syntax/src/Basic-Syntax/Reflection.purs
• Syntax/Type-Level-Programming-Syntax/src/Basic-Syntax/Reification.purs

Body

Hello there. First of all thanks for writing this, I have to say, it's probably one of the best documents on functional programming and especially purescript out there. One of the very few as well.

Now to the point, it's not a bug per session, more of an inconsistency and especially for beginners like myself it's hard enough to keep track of these things.

So in explaining type level programming, in the specified files you use Boolean as an example case. But in Reflection you use data Boolean_ = True_Value | False_Value which you end up not using, the implementation actually uses Boolean directly. I personally think Boolean_ is much better for beginners and it's in line with the used language so far. So this goes for Reification file as well. In the Reification file you end up using Boolean to begin with.

Another thing in Reflection is that some comments talk about BProxy but the implementation is with BooleanProxy. And even though it's longer, I think it's better to say BooleanProxy and BooleanProxyInstance instead of BProxy & BProxyInstance. The better consistency, the less confusing it becomes.

Thanks again!

[JordanMartinez]

Hello there. First of all thanks for writing this, I have to say, it's probably one of the best documents on functional programming and especially purescript out there. One of the very few as well.

Thanks!

I'm restating my understanding of your point. Please correct me where I'm misunderstanding you.

So in explaining type level programming, in the specified files you use Boolean as an example case. But in Reflection you use data Boolean_ = True_Value | False_Value which you end up not using, the implementation actually uses Boolean directly. I personally think Boolean_ is much better for beginners and it's in line with the used language so far. So this goes for Reification file as well. In the Reification file you end up using Boolean to begin with.

Specifically, in this line, I define a 'custom' Boolean type so that it appears similar to the CustomKind/CustomInstance idea mentioned in these lines. However, when I actually give examples of reflection in these lines, I don't use my 'custom' Boolean type but instead use the primitive type. This creates a moment of confusion to the learner because they were expecting to see the custom type used there, not the primitive one. Moreover, I do this again in the Reification file as well.

That's a good point. I originally only used Boolean_ to show that true/false are just instances of a type that happen to be primitive instances. I think you're point is valid and that it should be the default. However, should the example that uses the primitive boolean type be removed? What if it remained, but as a comment?

Another thing in Reflection is that some comments talk about BProxy but the implementation is with BooleanProxy. And even though it's longer, I think it's better to say BooleanProxy and BooleanProxyInstance instead of BProxy & BProxyInstance. The better consistency, the less confusing it becomes.

I agree with you here. It's not until the Conventions.purs file that I explain that the proxy type is abbreviated as [First letter of kind name]Proxy and that convention should only be explained and used there.

Would you mind submitting a PR that fixes those things?

[razcore-rad]

So yes, you got that right. I can do the PR, actually I was working on it and I came across an "issue". If you want to try out the example in the REPL to say check isTrue trueK or isTrue (BooleanProxyInstance :: BooleanProxy False) etc. then purescript will complain that there's no show instance for Boolean_. You have at the end of the file in some places this comment -- necessary to make this file compile, I was thinking one way of doing it is to provide the Show instance after a comment like -- necessary for you to play in the REPL without givin errors, it will be explained later or possibly something better and link in the package docs.

I think it might be confusing to have Boolean and Boolean_ while the topic can get confusing enough on its own because same terms are used in different and unrelated contexts. Adding on top of that might not be a great idea, but I'm not entirely convinced it's bad either, because up to this point there's not much "real working code" so to get some actual example using the native stuff might not be bad either.

As a side note, when I first started looking at purescript this Boolean threw me off quite a bit, because I was expecting it to be defined as data Boolean = True | False just like in haskell, and I was in the mindset that constructors have to start with a capital letter so I was very surprised to find true/false instead. I suppose it's because purescript targets javascript and it's a more "native" (in regards to javascript) approach. I think if you would talk about this issues it would possibly make some more sense when you see true/false and possibly I wouldn't feel as strong about having the examples with Boolean as well :)

edit
or rather the Show typeclass was explained previously, I just forgot

[JordanMartinez]

then purescript will complain that there's no show instance for Boolean_

Mm... I'm fine with you adding a Show constraint to make that work. I've already taken the -- necessary to compile/repl approach in prior cases, so it shouldn't be surprising to new learners.

I think it might be confusing to have Boolean and Boolean_ while the topic can get confusing enough on its own because same terms are used in different and unrelated contexts. Adding on top of that might not be a great idea, but I'm not entirely convinced it's bad either, because up to this point there's not much "real working code" so to get some actual example using the native stuff might not be bad either.

Good point. Well, the whole point of the folder is to teach the syntax. It's not really meant for 'real-world' examples. That's what the Hello World folder is for (and even that is lacking right now in such examples because I'm not sure what problems TLP specifically solve when we don't have backtracking).

Somewhat related to this, there are actually two versions of a type-level Boolean: one that uses kinds and one that uses data True and data False with a type class constraint to guarantee that a given type is one of those type-level instances. The latter is only possible because the number of instances of Boolean is so small.

I was in the mindset that constructors have to start with a capital letter so I was very surprised to find true/false instead. I suppose it's because purescript targets javascript and it's a more "native" (in regards to javascript) approach. I think if you would talk about this issues it would possibly make some more sense when you see true/false and possibly I wouldn't feel as strong about having the examples with Boolean as well :)

That's actually another issue worth discussing separately from this as it does break one's intuition. I think that should also be clarified. Mind opening a new issue for it?