Counterexamples in type systems

AF
Andy Fingerhut
Sun, May 23, 2021 7:12 PM

I happened across this web page recently.  I do not recall what I was
searching for at the time I came across it, but some of the examples seem
like they might be relevant to recent discussions in the P4 language design
work group regarding union types, switch statements that some have proposed
work similar to pattern matching in languages like Haskell/Ocaml/etc.
Perhaps these are well known examples, but wanted to pass them along in
case they are not:

https://counterexamples.org/

Andy Fingerhut

I happened across this web page recently. I do not recall what I was searching for at the time I came across it, but some of the examples seem like they might be relevant to recent discussions in the P4 language design work group regarding union types, switch statements that some have proposed work similar to pattern matching in languages like Haskell/Ocaml/etc. Perhaps these are well known examples, but wanted to pass them along in case they are not: https://counterexamples.org/ Andy Fingerhut
NF
Nate Foster
Mon, May 24, 2021 9:26 PM

Yeah, this is a great page. It really shows why type system design and
implementation can both be tricky.

One of these examples (Dubious Evidence) was mentioned before as a reason
to be cautious when adding generics to P4.

-N

On Sun, May 23, 2021 at 3:12 PM Andy Fingerhut andy.fingerhut@gmail.com
wrote:

I happened across this web page recently.  I do not recall what I was
searching for at the time I came across it, but some of the examples seem
like they might be relevant to recent discussions in the P4 language design
work group regarding union types, switch statements that some have proposed
work similar to pattern matching in languages like Haskell/Ocaml/etc.
Perhaps these are well known examples, but wanted to pass them along in
case they are not:

https://counterexamples.org/

Andy Fingerhut


P4-design mailing list -- p4-design@lists.p4.org
To unsubscribe send an email to p4-design-leave@lists.p4.org

Yeah, this is a great page. It really shows why type system design and implementation can both be tricky. One of these examples (Dubious Evidence) was mentioned before as a reason to be cautious when adding generics to P4. -N On Sun, May 23, 2021 at 3:12 PM Andy Fingerhut <andy.fingerhut@gmail.com> wrote: > I happened across this web page recently. I do not recall what I was > searching for at the time I came across it, but some of the examples seem > like they might be relevant to recent discussions in the P4 language design > work group regarding union types, switch statements that some have proposed > work similar to pattern matching in languages like Haskell/Ocaml/etc. > Perhaps these are well known examples, but wanted to pass them along in > case they are not: > > https://counterexamples.org/ > > Andy Fingerhut > _______________________________________________ > P4-design mailing list -- p4-design@lists.p4.org > To unsubscribe send an email to p4-design-leave@lists.p4.org >
MB
Mihai Budiu
Mon, May 24, 2021 10:14 PM

It also shows that even very experienced people get it wrong.

Mihai

From: Nate Foster jnfoster@gmail.com
Sent: Monday, May 24, 2021 2:26 PM
To: Andy Fingerhut andy.fingerhut@gmail.com
Cc: p4-design p4-design@lists.p4.org
Subject: [P4-design] Re: Counterexamples in type systems

Yeah, this is a great page. It really shows why type system design and implementation can both be tricky.

One of these examples (Dubious Evidence) was mentioned before as a reason to be cautious when adding generics to P4.

-N

On Sun, May 23, 2021 at 3:12 PM Andy Fingerhut <andy.fingerhut@gmail.commailto:andy.fingerhut@gmail.com> wrote:
I happened across this web page recently.  I do not recall what I was searching for at the time I came across it, but some of the examples seem like they might be relevant to recent discussions in the P4 language design work group regarding union types, switch statements that some have proposed work similar to pattern matching in languages like Haskell/Ocaml/etc.  Perhaps these are well known examples, but wanted to pass them along in case they are not:

https://counterexamples.org/https://nam04.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcounterexamples.org%2F&data=04%7C01%7Cmbudiu%40vmware.com%7C833b32113c904a682b8308d91efa97fa%7Cb39138ca3cee4b4aa4d6cd83d9dd62f0%7C0%7C1%7C637574883913677545%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=BR5NsGA%2BKTDU3knQ9ivMI1nJV05gtLmIKzhqmGVImio%3D&reserved=0

Andy Fingerhut


P4-design mailing list -- p4-design@lists.p4.orgmailto:p4-design@lists.p4.org
To unsubscribe send an email to p4-design-leave@lists.p4.orgmailto:p4-design-leave@lists.p4.org

It also shows that even very experienced people get it wrong. Mihai From: Nate Foster <jnfoster@gmail.com> Sent: Monday, May 24, 2021 2:26 PM To: Andy Fingerhut <andy.fingerhut@gmail.com> Cc: p4-design <p4-design@lists.p4.org> Subject: [P4-design] Re: Counterexamples in type systems Yeah, this is a great page. It really shows why type system design and implementation can both be tricky. One of these examples (Dubious Evidence) was mentioned before as a reason to be cautious when adding generics to P4. -N On Sun, May 23, 2021 at 3:12 PM Andy Fingerhut <andy.fingerhut@gmail.com<mailto:andy.fingerhut@gmail.com>> wrote: I happened across this web page recently. I do not recall what I was searching for at the time I came across it, but some of the examples seem like they might be relevant to recent discussions in the P4 language design work group regarding union types, switch statements that some have proposed work similar to pattern matching in languages like Haskell/Ocaml/etc. Perhaps these are well known examples, but wanted to pass them along in case they are not: https://counterexamples.org/<https://nam04.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcounterexamples.org%2F&data=04%7C01%7Cmbudiu%40vmware.com%7C833b32113c904a682b8308d91efa97fa%7Cb39138ca3cee4b4aa4d6cd83d9dd62f0%7C0%7C1%7C637574883913677545%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=BR5NsGA%2BKTDU3knQ9ivMI1nJV05gtLmIKzhqmGVImio%3D&reserved=0> Andy Fingerhut _______________________________________________ P4-design mailing list -- p4-design@lists.p4.org<mailto:p4-design@lists.p4.org> To unsubscribe send an email to p4-design-leave@lists.p4.org<mailto:p4-design-leave@lists.p4.org>
NF
Nate Foster
Tue, May 25, 2021 2:38 AM

Indeed, many of these are implementation not design bugs.

-N

On Mon, May 24, 2021 at 6:14 PM Mihai Budiu mbudiu@vmware.com wrote:

It also shows that even very experienced people get it wrong.

Mihai

From: Nate Foster jnfoster@gmail.com
Sent: Monday, May 24, 2021 2:26 PM
To: Andy Fingerhut andy.fingerhut@gmail.com
Cc: p4-design p4-design@lists.p4.org
Subject: [P4-design] Re: Counterexamples in type systems

Yeah, this is a great page. It really shows why type system design and
implementation can both be tricky.

One of these examples (Dubious Evidence) was mentioned before as a reason
to be cautious when adding generics to P4.

-N

On Sun, May 23, 2021 at 3:12 PM Andy Fingerhut andy.fingerhut@gmail.com
wrote:

I happened across this web page recently.  I do not recall what I was
searching for at the time I came across it, but some of the examples seem
like they might be relevant to recent discussions in the P4 language design
work group regarding union types, switch statements that some have proposed
work similar to pattern matching in languages like Haskell/Ocaml/etc.
Perhaps these are well known examples, but wanted to pass them along in
case they are not:

https://counterexamples.org/
https://nam04.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcounterexamples.org%2F&data=04%7C01%7Cmbudiu%40vmware.com%7C833b32113c904a682b8308d91efa97fa%7Cb39138ca3cee4b4aa4d6cd83d9dd62f0%7C0%7C1%7C637574883913677545%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=BR5NsGA%2BKTDU3knQ9ivMI1nJV05gtLmIKzhqmGVImio%3D&reserved=0

Andy Fingerhut


P4-design mailing list -- p4-design@lists.p4.org
To unsubscribe send an email to p4-design-leave@lists.p4.org

Indeed, many of these are implementation not design bugs. -N On Mon, May 24, 2021 at 6:14 PM Mihai Budiu <mbudiu@vmware.com> wrote: > It also shows that even very experienced people get it wrong. > > > > Mihai > > > > *From:* Nate Foster <jnfoster@gmail.com> > *Sent:* Monday, May 24, 2021 2:26 PM > *To:* Andy Fingerhut <andy.fingerhut@gmail.com> > *Cc:* p4-design <p4-design@lists.p4.org> > *Subject:* [P4-design] Re: Counterexamples in type systems > > > > Yeah, this is a great page. It really shows why type system design and > implementation can both be tricky. > > > > One of these examples (Dubious Evidence) was mentioned before as a reason > to be cautious when adding generics to P4. > > > > -N > > > > On Sun, May 23, 2021 at 3:12 PM Andy Fingerhut <andy.fingerhut@gmail.com> > wrote: > > I happened across this web page recently. I do not recall what I was > searching for at the time I came across it, but some of the examples seem > like they might be relevant to recent discussions in the P4 language design > work group regarding union types, switch statements that some have proposed > work similar to pattern matching in languages like Haskell/Ocaml/etc. > Perhaps these are well known examples, but wanted to pass them along in > case they are not: > > > > https://counterexamples.org/ > <https://nam04.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcounterexamples.org%2F&data=04%7C01%7Cmbudiu%40vmware.com%7C833b32113c904a682b8308d91efa97fa%7Cb39138ca3cee4b4aa4d6cd83d9dd62f0%7C0%7C1%7C637574883913677545%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=BR5NsGA%2BKTDU3knQ9ivMI1nJV05gtLmIKzhqmGVImio%3D&reserved=0> > > > > Andy Fingerhut > > _______________________________________________ > P4-design mailing list -- p4-design@lists.p4.org > To unsubscribe send an email to p4-design-leave@lists.p4.org > >