Self driving twizy

Я тут недавно писал, что озолотится тот, кто сделает Self-driving Renault Twizy в качестве такси без водителя, потому что водителю платить не надо, потребление в районе 5kWh/100km электричества из любой розетки, и сама машинка совершенно недорогая.

Но есть соображение, что Self driving cars ещё десятилетия будут ездить слишком медленно и осторожно, так есть же очевидный выход: если у пассажира есть права и нет алкогольного опьянения, то можно разрешить ему рулить. А в режиме автовождения можно ограничить скорость автомобиля какими-нибудь там супер-безопасными 30км/ч, чтобы получить государственные разрешения как можно быстрее. Тогда это будет революция скорее не в такси-бизнесе, а в бизнесе каршеринга. Каршеринговая машинка, которая сама (хоть и медленно) приезжает туда, где её хочешь взять, и сама уезжает оттуда, где её оставил.

Инкапсюляция

В MLTT нет способа гибко скрывать реализацию интерфейсов, но, как я только что понял, его очень легко туда добавить.

Вот смотрите, чтобы применить f(x) : A -> B к значению x : A', нужно чтобы A ≡ A', где ≡ это подстановочное равенство. Обычно оно делается так: определения A и A' нужно привести в нормальную форму, а затем сравнить “побуквенно“ (с точностью до альфа-конверсий).

Чтобы добавить information hiding, достаточно добавить в язык возможность ограничивать подстановочное равенство. То есть добавить в язык операцию номинальной инкапсюляции
Name := definition, с двумя свойствами: во-первых одно имя можно применить только один раз, во вторых x ≡ Name тогда и только тогда, когда x и есть Name, в частности невыводимо, что Name ≡ definition (хотя на propositional-уровне, конечно, Name = definition).

Например можно сделать Nat := \container Boolean (\n : Type => (tt => n, ff => (n -> n)))). Можно определить и AnotherNat := \container Boolean (\n : Type => (tt => n, ff => (n -> n)))), с таким же определением, однако применить функцию f: Nat -> Something к значению x : AnotherNat не удастся, не определив конверсию в явном виде.

Теперь для полноты счастья хочется усилить _≡_ в духе OTT для П-типов и сразу получить таким образом path dependent types. С другой стороны (независимо от этого) можно добавить конструкцию Name := \refine[AnotherName] (определение орнамента) и ослабить условие рефлексивности _≡_, обретая таким образом manifest subtyping, но с этим нужно аккуратно.