(no subject)

Просто вялые размышления о динамической типизации и зависимых типах.

подумал, что языки с динамической типизацией -- это как бы "языки с зависимыми типами". например,

function add(a, b) { return (a + b); };

вполне можно записать как

add : Ta : Type -> a : Ta -> Tb : Type -> b : Tb -> Ta =
if Ta = Number
then add_number a (cast_to_number Tb b)
else if Ta = String
then concat a (cast_to_string Tb b)
else fail

, в случаях, когда определены

cast_to_number : T : Type -> x : T -> number
cast_to_string : T : Type -> x : T -> string

Фактически, любое значение имеет ассоциированный с ним в рантайме тип, и можно было бы в примере выше передавать сразу (Ta : Type, a : Ta) в виде туплов.
Однако, если с add было понятно, что вернётся значение с типом Ta, то в случае неизвестного типа будет возвращён именно тупл (T:Type, x:T), но не простой, а с проставленными ограничениями (именно: второй компонент имеет тип, равный первому компоненту). А как такое рассматривать -- пока не знаю. Кто-нибудь ковырял языки с зависимыми типами? Должен быть, по идее, штатный подход.