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

spec: subtype checking only for reference types #311

Merged
merged 8 commits into from
Dec 4, 2022

Conversation

chenyan-dfinity
Copy link
Contributor

Fix #295

spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
spec/Candid.md Show resolved Hide resolved
spec/Candid.md Outdated Show resolved Hide resolved
nomeata added a commit to nomeata/candid that referenced this pull request Feb 10, 2022
@nomeata
Copy link
Collaborator

nomeata commented Feb 10, 2022

#316 has early explorations of updating the Coq proof for this, but stuck at various technicalities right now. For example

Lemma coerce_roundtrip:
  forall t1 v1,
  v1 :: t1 ->
  coerce t1 t1 v1 = Some v1.

doesn't work with our “untyped values” in the formalization because :: allows any reference value at any type.

spec/Candid.md Outdated Show resolved Hide resolved
Co-authored-by: Claudio Russo <[email protected]>
spec/Candid.md Outdated Show resolved Hide resolved
@nomeata
Copy link
Collaborator

nomeata commented Oct 7, 2022

Oh, this hasn't landed yet? Completely forgot… I guess we are waiting for all implementations to catch up?

@crusso
Copy link
Contributor

crusso commented Oct 26, 2022

Oh, this hasn't landed yet? Completely forgot… I guess we are waiting for all implementations to catch up?

@chenyan-dfinity is working on it. Motoko is hopefully ready to go (though I'm worried even I don't understand that implementation any more).

Co-authored-by: Claudio Russo <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
@chenyan-dfinity chenyan-dfinity marked this pull request as ready for review December 4, 2022 22:31
@chenyan-dfinity chenyan-dfinity merged commit 6edd82f into master Dec 4, 2022
@chenyan-dfinity chenyan-dfinity deleted the spec-variant branch December 4, 2022 22:39
@nomeata
Copy link
Collaborator

nomeata commented Dec 5, 2022

🥳

I have released haskell-candid 0.4 with the corresponding changes (nomeata/haskell-candid#20).

Maybe someone can help me with dfinity/ic-hs#118?

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

Successfully merging this pull request may close these issues.

Extensible variants
3 participants