5 ms·
> At least TypeOK can be much more expressive than any type system. Can you clarify what you mean by that? Dependent types or more practically refinement types
by deredede 1y ago
> At least TypeOK can be much more expressive than any type system.
Can you clarify what you mean by that? Dependent types or more practically refinement types (à la F*) can embed arbitrary predicates.
- _flux 1y agoRight, I was referring totype systems in relatively popular real-world programming languages of today, i.e. Haskell, OCaml, Rust, Haskell :).