Skip to content

Added thunk-syntax to mimic syntax for products etc #528

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

Merged
merged 2 commits into from
Nov 12, 2018
Merged

Added thunk-syntax to mimic syntax for products etc #528

merged 2 commits into from
Nov 12, 2018

Conversation

oisdk
Copy link
Contributor

@oisdk oisdk commented Nov 9, 2018

This adds a syntax declaration for Thunks. It mimics the syntax declarations for Σ. I found myself using a lot of sized types where the size parameter was implicit, or where it wasn't the last parameter, and this syntax would make things a little easier to read. Take this example of a coinductive non-empty list:

With syntax:

record NonEmpty {i : Size} {a} (A : Set a) : Set a where
  coinductive
  field
    head : A
    tail : Maybe (Thunk[ j < i ] NonEmpty {j} A)

Without syntax:

record NonEmpty {i : Size} {a} (A : Set a) : Set a where
  coinductive
  field
    head : A
    tail : Maybe (Thunk (λ j  NonEmpty {j} A) i)

@gallais
Copy link
Member

gallais commented Nov 9, 2018

Orthogonal remarks:

  • your NonEmpty is Stream. I hadn't seen the Maybe. I still think you probably want the Thunk-ed thing to be a Colist instead
  • the recommended practice is to have the Size explicit in the type

Edit: btw it'd be nice to have non-empty colists in the stdlib too.

@gallais gallais added this to the v0.18 milestone Nov 9, 2018
@MatthewDaggitt MatthewDaggitt merged commit 38409f0 into agda:master Nov 12, 2018
@MatthewDaggitt
Copy link
Contributor

Thanks for the PR!

@MatthewDaggitt MatthewDaggitt modified the milestones: v0.18, v1.0 Feb 22, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants