[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Thanks, Neel and others, for raising the issue. I think we all agree that
the registration costs are higher than we would have liked, but let me also
point out that we live in interesting times, and the past few years
this lemma by induction on typing:
>
> K[e] : B <=> ∃ A, e : A ∧ ∀ e, e : A => K[e] : B.
>
> Jules
>
>
> On Sat, Oct 9, 2021 at 11:14 PM Derek Dreyer wrote:
>>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>
\ and Senior Research Fellow, IOHK
> .
> https://urldefense.com/v3/__http://homepages.inf.ed.ac.uk/wadler/__;!!IBzWLUs!G2KhnZbuiPIsnAWmxp3nKsyAqqNkyiHo5kL0icZ3pru8QkU69To1o-Oz6FUAk52G_lp8h6qNokQ$
>
>
>
>
> On Sat, 9 Oct 2021 at 22:12, Derek Dreyer wrote:
>&
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi, Phil.
Yes, there is a way to make the single congruence rule work. See for
example the way I set things up in my Semantics course notes (see
Section 1.2):
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> Further, ACM does many positive things beyond archiving articles.
According to Crista Lopes on Twitter (I'm not sure if she's on this list):
"I studied @TheOfficialACM’s finances a few years ago, when I was
Treasurer
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi, Sam.
I would take issue with your characterization of this example as
"breaking abstraction". By way of analogy, when you opaquely seal a
module with a signature containing a field
val v : T,
it does not mean
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
To inject a different point of view into this discussion:
There's a lot more to the interaction of different type system
features than just how the combination of those features affects
typechecking, type soundness,
