Dependent Types and How to Get Rid of Them

Re:Dependent Types and How to Get Rid of Them by tome on Wednesday November 12, 2025 @11:38AM (#45902253)

Hmm, maybe

> most type theories don't enforce full parametricity at runtime

means "sometimes types can appear at run time"? If so it's true, but it's not what I understand by "parametricity".

[ Parent | on HN ]

Re:Dependent Types and How to Get Rid of Them by aatd86 on Wednesday November 12, 2025 @01:29PM (#45903883)

Not sure, either : Parametric polymorphism is compile time. Adding runtime behaviors is a sort of escape hatch.

Which is fair although necessary. It's not so much a breakage as it is a necessity, since non parametric code may rely on this too.

Or maybe it is about constrained parametricity. In any case this doesn't seem a big issue.

[ Parent | on HN ]