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.

Sign up for GitHub

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

Jump to bottom

instance args #3

Merged
merged 11 commits into from
Dec 3, 2020
Merged

instance args #3

merged 11 commits into from
Dec 3, 2020

Conversation

jmchapman
Copy link
Contributor

@jmchapman jmchapman commented Oct 22, 2020 •
edited
Loading

  • (first attempt at) converting instances args to constraints in type sigs
  • not expanding instance usage in clause bodies
  • type classes
  • instances
  • Dealing with typically derived stuff like Show

@UlfNorell UlfNorell mentioned this pull request Oct 22, 2020
Merged
UlfNorell
UlfNorell reviewed Oct 23, 2020
View reviewed changes
Main.hs Outdated Show resolved Hide resolved
@jmchapman
Merge branch 'master' of https://github.com/agda/agda2hs into instanc…
6e3f6cb 
…e-args
@jmchapman
Merge branch 'master' of https://github.com/agda/agda2hs into instanc…
729dfc2 
…e-args
@jmchapman
processPragma
36fde50 
This commit is just recording where we got to this morning on deteching a
"class" pragma on a record.

The tests currently fail as the RHSs of sumMon contain "M.f r" instead of "f".
@jmchapman
A first attempt dealing with instance arg usage (record projections) …
20e2929 
…on the RHS

This works for the example but is a hack.

1. Assume any record projection is a usage of an instance arg.
2. Strip the module prefix off the name.
3. Eat the first visible argument which is the record.

All 3 should be done better.
@jmchapman
generating a type class decl (parameters and field types missing)
a61bbdd 
class Monoid @0 where
        mempty :: *
        mappend :: *

I am not sure why the class parameter is rendered as @0 and I need to find where to extract the field types from
@jmchapman
type class: parameter names show up, field types shown names are not …
75177e4 
…correct

class Monoid a where
        mempty :: @0
        mappend :: @1 -> @1 -> @1

I need to work out how to instantiate the telescope that holds the
parameters and fields
@UlfNorell
Copy link
Member

Try a combination of telViewUpTo, recPars, defType to get the parameter telescope. Check what I do in compileClause to get it into the context.

@jmchapman
Copy link
Contributor Author

Thanks, I'll give that shot!

@jmchapman
example type class def correctly compiled:
c793afd 
class Monoid a where
        mempty :: a
        mappend :: a -> a -> a
@omelkonian omelkonian mentioned this pull request Nov 24, 2020
Merged
@UlfNorell
Copy link
Member

Would it make sense to limit the scope of this PR and try to get it merged in its current stage (pending merge conflicts)? Just having the translation of class constraints and proper handling of calls to member functions lets you work with the Prelude type classes.

@jmchapman
Copy link
Contributor Author

jmchapman commented Dec 1, 2020 •
edited
Loading

Yes, good idea. Apologies for blocking this feature (and the prelude). I am planning to get back to agda2hs tomorrow.

I added some support for compiling record declarations into type classes. I haven't dealt with compiling instances of those records to type class instances or picking up deriving on datatypes. This could be handled in a separate PR.

@jmchapman jmchapman force-pushed the instance-args branch 5 times, most recently from ba24d87 to d7ff9bf Compare December 2, 2020 17:17
@jmchapman jmchapman marked this pull request as ready for review December 2, 2020 17:26
@jmchapman
Copy link
Contributor Author

I did a merge. The things I have done should probably be made more robust/flexible but perhaps it's already useful?

@jmchapman jmchapman self-assigned this Dec 2, 2020
@UlfNorell UlfNorell merged commit 5e658a7 into master Dec 3, 2020
@UlfNorell UlfNorell deleted the instance-args branch December 3, 2020 07:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@UlfNorell UlfNorell UlfNorell approved these changes

Assignees

@jmchapman jmchapman

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@jmchapman @UlfNorell