Skip to content

spec: subtype checking only for reference types#311

Merged
chenyan-dfinity merged 8 commits into
masterfrom
spec-variant
Dec 4, 2022
Merged

spec: subtype checking only for reference types#311
chenyan-dfinity merged 8 commits into
masterfrom
spec-variant

Conversation

@chenyan-dfinity

Copy link
Copy Markdown
Contributor

Fix #295

Comment thread spec/Candid.md Outdated
Comment thread spec/Candid.md Outdated
Comment thread spec/Candid.md Outdated
Comment thread spec/Candid.md Outdated
Comment thread spec/Candid.md Outdated
Comment thread spec/Candid.md
Comment thread spec/Candid.md Outdated
Comment thread spec/Candid.md Outdated
Comment thread spec/Candid.md
Comment thread spec/Candid.md Outdated
Comment thread spec/Candid.md
Comment thread spec/Candid.md Outdated
Comment thread spec/Candid.md
Comment thread spec/Candid.md Outdated
chenyan-dfinity and others added 2 commits January 13, 2022 13:45
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Comment thread spec/Candid.md
Comment thread spec/Candid.md
nomeata added a commit to nomeata/candid that referenced this pull request Feb 10, 2022
@nomeata

nomeata commented Feb 10, 2022

Copy link
Copy Markdown
Contributor

#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.

Comment thread spec/Candid.md Outdated
Co-authored-by: Claudio Russo <claudio@dfinity.org>
Comment thread spec/Candid.md Outdated
@nomeata

nomeata commented Oct 7, 2022

Copy link
Copy Markdown
Contributor

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

@crusso

crusso commented Oct 26, 2022

Copy link
Copy Markdown
Contributor

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 <claudio@dfinity.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
@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

nomeata commented Dec 5, 2022

Copy link
Copy Markdown
Contributor

🥳

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