Refactor syntax/type level programming to YesNo #151

razcore-rad · 2018-11-21T20:22:10Z

(Added by Jordan): This change was introduced due to discussion in #139

JordanMartinez

Thanks for getting to this so quickly.

A few things should be renamed to better distinguish the value-level and type-level instances. There's also a few instance names that need to be renamed. Other than that, it looks good.

JordanMartinez · 2018-11-21T20:25:35Z

11-Syntax/03-Type-Level-Programming-Syntax/src/02-Basic-Syntax/01-Defining-Custom-Kinds.purs


-foreign import kind Boolean
+foreign import kind YesNo


The way this is defined, it's hard to see the difference between then YesNo type and the YesNo kind. Elsewhere in this PR, you use YesNoKind, which is correct and which I'd prefer.

I would say that this change should then propagate throughout and then we should have

foreign import kind YesNoKind foreign import data YesK :: YesNoKind foreign import data NoK :: YesNoKind

as well, shouldn't we? Otherwise the Yes/No might get confused with the value-level instances

I replied to your later comment, but stating it again here: yes, let's do it that way.

JordanMartinez · 2018-11-21T20:29:40Z

11-Syntax/03-Type-Level-Programming-Syntax/src/02-Basic-Syntax/01-Defining-Custom-Kinds.purs

@@ -19,11 +19,11 @@ foreign import data Value_Level_Instance2 :: Value_Level_Type_Kind
 -- despite the "foreign import" syntax!
 ----------------------

-- Using the value-level type Boolean as an example...
-data Boolean_ = True_Value | False_Value
+-- Using a Boolean-like value-level type as an example...


I like that you have referred to Boolean here as the analogy of YesNo. However, it will likely make others wonder why Boolean itself wasn't just used, leading them to open a new issue.

Perhaps this comment should include a link to the corresponding issue?

The reason I don't think it would be too problematic is that you already talk about the fact that Boolean is an internal type and you change slightly the names in some places so there's no overlap. But sure, once we get the Boolean info written it won't hurt to have a link

JordanMartinez · 2018-11-21T20:31:04Z

11-Syntax/03-Type-Level-Programming-Syntax/src/02-Basic-Syntax/01-Defining-Custom-Kinds.purs

-foreign import data True :: Boolean
-foreign import data False :: Boolean
+foreign import data Yes :: YesNo
+foreign import data No :: YesNo


This no longer distinguishes the instance (e.g. data YesNo = Yes) from the type (e.g. kind YesNoKind = Yes).

Perhaps we should distinguish it like this...?

data YesNo = Yes_Value | No_Value foreign import kind YesNoKind foreign import data Yes :: YesNoKind foreign import data No :: YesNoKind

How about going with

data YesNo = Yes | No foreign import kind YesNoKind foreign import data YesK :: YesNoKind foreign import data NoK :: YesNoKind

like I mentioned in the first comment?

Yes, that sounds good.

JordanMartinez · 2018-11-21T20:32:05Z

...ng-Syntax/src/02-Basic-Syntax/03-Defining-Functions/03-Pattern-Matching-Using-Instances.purs

-instance toInt_FalseZero :: ToInt False Zero
+class ToInt (input :: YesNo) (output :: ZeroOrOne) | input -> output
+instance toInt_TrueOne :: ToInt Yes One
+instance toInt_FalseZero :: ToInt No Zero


These instances should be renamed to toInt_YesOne and toInt_NoZero

Yep, missed these

JordanMartinez · 2018-11-21T20:33:23Z

11-Syntax/03-Type-Level-Programming-Syntax/src/02-Basic-Syntax/04-Reflection.purs

+foreign import kind YesNoKind
+foreign import data Yes :: YesNoKind
+foreign import data No  :: YesNoKind
+data YesNoProxy (a :: YesNoKind) = YesNoProxyInstance


(I'm including this comment in case the question comes to mind due to other renaming comments in this review)

This could be renamed to YesNoKindProxy, but I think that's unnecessary. So, I think this should be left as you have it now.

razcore-rad · 2018-11-22T22:40:32Z

Amended the commit to include changes we discussed, hope I didn't miss any line, if you see something missing let me know.

closes #152

edit
the extra amends are for little fixes like changing YesNoK in one sole instance to YesNoKind etc.

JordanMartinez

Looks like you missed two things. Just push another commit that fixes that. No need to clean up the commit history since I can squash the commit into one.

JordanMartinez · 2018-11-23T22:35:27Z

11-Syntax/03-Type-Level-Programming-Syntax/src/02-Basic-Syntax/05-Reification.purs

-foreign import data False :: BooleanKind
+foreign import kind YesNoKind
+foreign import data Yes :: YesNoKind
+foreign import data No  :: YesNoKind


Looks like you forgot to use the same name scheme (YesK/NoK)

JordanMartinez · 2018-11-23T22:37:39Z

11-Syntax/03-Type-Level-Programming-Syntax/src/02-Basic-Syntax/05-Reification.purs

-falseK :: BooleanProxy False
-falseK = BooleanProxyInstance
+noK :: YesNoProxy No
+noK = YesNoProxyInstance


and update the YesNoProxy [Yes/No] to [YesK/NoK] here, too.

razcore-rad · 2018-11-24T09:44:56Z

While applying the last fixes I found out that the example with toRed/toBlue doesn't work:

> :p
… toRed :: YesNoProxy YesK -> String
… toRed _ = "red"
…
> reifyYesNo Yes toRed
Error found:
in module $PSCI
at  line 1, column 16 - line 1, column 16

  Could not match type

    b0

  with type

    YesK


while trying to match type YesNoProxy b0
  with type YesNoProxy YesK
while checking that expression toRed
  has type YesNoProxy b0 -> t1
in value declaration it

where b0 is a rigid type variable
        bound at line 1, column 16 - line 1, column 16
      t1 is an unknown type

See https://github.com/purescript/documentation/blob/master/errors/TypesDoNotUnify.md for more information,
or to contribute content related to this error.

And I'm sure it's because of YesNoKindConstraint. If you change the type signature to something like toRed :: forall b. YesNoKindConstraint b => YesNoProxy b -> String it works but I'm not sure it's the right thing to do?

I'm not sure why this is happening, shouldn't instance yesYesNo :: IsYesNoKind YesK take care of the constraint?

JordanMartinez · 2018-11-24T17:15:42Z

While applying the last fixes I found out that the example with toRed/toBlue doesn't work

Those aren't supposed to work (hence why they are commented out). I wrote that section when I didn't fully understand how that concept (using type-level functions to compute things via unification) was even possible.

Sometime later, I wrote this file, which shows why that idea is actually accurate. This PR reminded me that I hadn't fixed that explanation yet, so I was hoping to fix it after you finished the PR.

Edit: Thus, toRed and toBlue are value-level functions which should be converted into type-level functions via type constraints ToColor input output => whose only instances are:

ToColor YesK Red
ToColor NoK Blue

razcore-rad · 2018-11-24T17:34:52Z

Alright then, I think I'm done fixing all the stuff we discussed so far so you can hopefully merge this now so we can get to the next thing

JordanMartinez · 2018-11-24T17:37:31Z

Looks good. Thanks for your contribution!

JordanMartinez requested changes Nov 21, 2018

View reviewed changes

JordanMartinez requested changes Nov 23, 2018

View reviewed changes

Refactor syntax/type level programming to YesNo

1ea5d34

JordanMartinez merged commit 67eeed2 into JordanMartinez:latestRelease Nov 24, 2018

JordanMartinez mentioned this pull request Nov 25, 2018

Type level programming defining kinds bug #152

Closed

razcore-rad deleted the yesno_typelevel branch November 25, 2018 10:40

JordanMartinez mentioned this pull request Nov 27, 2018

Explain why type-level reification defines forall separately #157

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor syntax/type level programming to YesNo #151

Refactor syntax/type level programming to YesNo #151

razcore-rad commented Nov 21, 2018 •

edited by JordanMartinez

JordanMartinez left a comment

JordanMartinez Nov 21, 2018

razcore-rad Nov 21, 2018 •

edited

JordanMartinez Nov 21, 2018

JordanMartinez Nov 21, 2018

razcore-rad Nov 21, 2018

JordanMartinez Nov 21, 2018

razcore-rad Nov 21, 2018

JordanMartinez Nov 21, 2018

JordanMartinez Nov 21, 2018

razcore-rad Nov 21, 2018

JordanMartinez Nov 21, 2018

razcore-rad commented Nov 22, 2018 •

edited

JordanMartinez left a comment

JordanMartinez Nov 23, 2018

JordanMartinez Nov 23, 2018

razcore-rad commented Nov 24, 2018 •

edited

JordanMartinez commented Nov 24, 2018 •

edited

razcore-rad commented Nov 24, 2018

JordanMartinez commented Nov 24, 2018

Refactor syntax/type level programming to YesNo #151

Refactor syntax/type level programming to YesNo #151

Conversation

razcore-rad commented Nov 21, 2018 • edited by JordanMartinez

JordanMartinez left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

razcore-rad Nov 21, 2018 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

razcore-rad commented Nov 22, 2018 • edited

JordanMartinez left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

razcore-rad commented Nov 24, 2018 • edited

JordanMartinez commented Nov 24, 2018 • edited

razcore-rad commented Nov 24, 2018

JordanMartinez commented Nov 24, 2018

razcore-rad commented Nov 21, 2018 •

edited by JordanMartinez

razcore-rad Nov 21, 2018 •

edited

razcore-rad commented Nov 22, 2018 •

edited

razcore-rad commented Nov 24, 2018 •

edited

JordanMartinez commented Nov 24, 2018 •

edited