Есть ли примеры добрых систем логического вывода с подтипами?В системах типов, таких как Haskell, нет никакого полиморфизма на добром слое.Как правило, вывод типов с параметрическим полиморфизмом является сложной проблемой, но поскольку виды не являются полиморфными, это сделало бы возможным вывод вида с подтипированием?
В частности, я думаю о видах в контексте расширяемых записей.Как и в «Расширяемых записях с метками в области» на бумаге или PureScript .
Я думаю, что такая грамматика:
k ::= * kind of term types
| record kind of record types
Где record - это подтип * в правилах набора текста.