Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Example/Simple.hs doesn't compile #15

Closed
gelisam opened this issue Jul 17, 2022 · 4 comments
Closed

Example/Simple.hs doesn't compile #15

gelisam opened this issue Jul 17, 2022 · 4 comments

Comments

@gelisam
Copy link

gelisam commented Jul 17, 2022

I first had to remove -Werror from plutarch-core.cabal in order to get past this unrelated error:

$ cabal repl
[...]
*** Exception: The following packages were specified via -package or -package-id flags,
but were not needed for compilation:
  - generics-sop-0.5.1.2-06250a69f3fc2d522ae418e9289393f2a0f8235347abce6b0b8887d14a0234a9
  - data-fix-0.3.2-b9f47d59a8d3a40a6cab9330e980f581afb5026ee9bb16169dc8c0f5e15586f4
  - base-4.16.0.0

Then I got an unbound identifier when loading the example:

$ cabal repl
λ> :load Examples/Simple.hs 
[...]
Examples/Simple.hs:17:80: error:
    Not in scope: type constructor or class ‘UnEf’
   |
17 | newtype EForall1 (f :: EType -> EType) ef = EForall1 (Ef ef (EForall (IsEType (UnEf ef)) f))
   |                                                                                ^^^^

Looking at the history, looks like the UnEf type family was renamed to EfC in 8975df7.

After performing the rename, I get a kind error instead:

Examples/Simple.hs:17:80: error:
    • Couldn't match kind ‘ETypeF -> Type’ with ‘ETypeRepr’
      Expected kind ‘EDSLKind’,
        but ‘EfC ef’ has kind ‘EType -> Constraint’
    • In the first argument of ‘IsEType’, namely ‘(EfC ef)’
      In the first argument of ‘EForall’, namely ‘(IsEType (EfC ef))’
      In the second argument of ‘Ef’, namely
        ‘(EForall (IsEType (EfC ef)) f)’
   |
17 | newtype EForall1 (f :: EType -> EType) ef = EForall1 (Ef ef (EForall (IsEType (EfC ef)) f))
   |                                                                                ^^^^^^

Looking at the kinds involved, I can fix the kind error by replacing IsEType (EfC ef) with EfC ef, but I don't yet have any idea if that makes any sense semantically.

With that "fix", I next encounter a type error:

Examples/Simple.hs:38:10: error:
    • Couldn't match type: EUnit f0
                     with: Term edsl EUnit
      Expected: Ef (Plutarch.Core.Helper edsl) U0
        Actual: EUnit f0
    • In the pattern: EUnit
      In the pattern: ERight EUnit
      In a case alternative: ERight EUnit -> econ EUnit
    • Relevant bindings include
        x :: Term edsl U1 (bound at Examples/Simple.hs:37:3)
        f :: Term edsl U1 -> Term edsl U0
          (bound at Examples/Simple.hs:37:1)
   |
38 |   ERight EUnit -> econ EUnit

That is, ERight's parameter is already a Term edsl EUnit, which is what we need on the right-hand-side, so the code can be simplified to:

f x = ematch x \case
  ERight eUnit -> eUnit
  ELeft eUnit -> eUnit 

With this second fix, Example/Simple.hs finally typechecks! However, the simplified code is not quite equivalent to the previous code, because we are no longer pattern-matching on EUnit. I get the impression that when the example was written, it was possible to write nested patterns with ematch, but that since then, ematch has been simplified so that only the outermost constructor is concretized. Thus, if we also want to match on the EUnit inside the ERight, we need a second ematch call:

f x = ematch x \case
  ERight eUnit -> ematch eUnit \case
    EUnit -> econ EUnit
  ELeft eUnit -> ematch eUnit \case
    EUnit -> econ EUnit
@L-as
Copy link
Member

L-as commented Aug 7, 2022

Thank you for taking a look at this! Sorry for the late reply.
@gelisam the example isn't really an example, it was me playing around and committing it.
Plutarch 2.0 is still not really ready, notably, I'm still trying to figure out how to make embedded data kinds work. This
is relevant to EForall and such, because really, it should be type EForall :: (a -> EType) -> EType.
The question is, what constraint do you use? You want to use IsEType, but it has to be more general.
It has to support types, higher types (e.g. Maybe), but we also want it to support data kinds.
This is not as trivial as it sounds, because generics only work at the value-level. Perhaps the solution is to abandon generics,
but I'm not quite ready for that.
Albeit, besides the generics stuff, it is pretty settled. I'll probably push the code sometime soon.

Wrt. nested matching, I abandoned this because it didn't seem worth it IMO. It gets very complex, and you have to do all sorts of magic to make it work, either using tons of type classes or using unsafePerformIO.
It's especially complex when you consider nested constructing.

As you might have noticed, we have an optics draft PR: #13 . Optics seem to solve the same ergonomicity issue AFAICT.

Thanks for showing interest though.

@L-as
Copy link
Member

L-as commented Aug 7, 2022

Wrt. doing cabal repl BTW, you're supposed to do cabal repl --repl-options=-Wwarn, albeit the warning in question is a bug in GHC I'm pretty sure, since it's completely bogus.

@L-as
Copy link
Member

L-as commented Aug 10, 2022

I fixed the examples (and commented out what doesn't work yet).

@gelisam
Copy link
Author

gelisam commented Aug 10, 2022

Thanks!

@gelisam gelisam closed this as completed Aug 10, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants