Типы и типы

[metaclass]

Очевидно ли, почему flatten и (partial apply concat) в Clojure могут выдать разные результаты? После хаскеля кложурный flatten, работающий на все уровни "вглубь", выглядит непривычно.

По ходу, статическая типизация делает невозможными некоторые типы программ, возможные при динамической.
Соответственно, наиболее заебатая статическая типизация, с какими-нибудь адскими зависимыми типами, должна делать невозможными еще большее количество программ.
А самая правильная типизация - это при которой множество допустимых программ пустое.

Comments

[thesz.livejournal.com]

Вот именно.

И к заявлениям metaclass: зависимые типы делают большее количество программ допустимыми.

[metaclass.livejournal.com]

Мы тут с theiced на эту тему спорили. Он привел пример вроде

charAt s i = s.[i]

по идее, никакая статическая типизация не поможет доказать, что эта функция не кинет исключения при выходе за пределы массива.
Т.е. программа то остается возможной, но все равно придется ее прогонять через юнит-тесты, и статическая типизация не поможет от них избавится.

[thesz.livejournal.com]

Это же на Хаскеле даже можно сделать.

Кстати, пример с корректной адресацией элементов массива идёт не то первым, не то вторым примером в какой-то из статей про Эпиграм. Вот трансляция оттуда в Хаскель по памяти:

{-# LANGUAGE GADTs #-}

data Zero = Zero
data Succ n = Succ n

data Vec len a where
	Nil :: Vec Zero a
	Con :: a -> Vec len a -> Vec (Succ len) a

data NatUp up where
	Z :: NatUp (Succ len)
	S :: NatUp len -> NatUp (Succ len)

charAt :: Vec len Char -> NatUp len -> Char
charAt (Con c _) Z = c
charAt (Con _ v) (S n) = charAt v n

good = charAt (Con 'a' Nil) Z
--bad = charAt (Con 'a' Nil) (S Z) -- не пройдёт!!!

[metaclass.livejournal.com]

О.
Т.е. если мы вводим s пользователем, то полный тип программы выведется только после ввода строки, или не выведется, потому что пользователь ввел "a" а мы обращаемся ко второму символу.
Соответственно, вместо обработки исключений в рантайме у нас вывод типов в рантайме, причем нужно еще куда-то сунуть локализуемое сообщение об ошибке, чтобы его показать пользователю.

Это можно сделать на зависимых типах?

[thesz.livejournal.com]

>Т.е. если мы вводим s пользователем, то полный тип программы выведется только после ввода строки, или не выведется, потому что пользователь ввел "a" а мы обращаемся ко второму символу.

Нет.

Вычислительная часть программы требует некоторых гарантий, и в той части программы, что занимается вводом данных мы должны произвести необходимые действия для проверки гарантий.

Гарантии указаны в типе. Контракте, если изволите.

Нарушение контракта можно переводить в сообщение об ошибке.

[metaclass.livejournal.com]

А, пользователю просто нельзя дать ввести строку, короче, чем мы к ней обращаемся. Мы ее просто никак не скастуем к допустимому для системы типу.

[thesz.livejournal.com]

Именно так.

[si14.livejournal.com]

Посмотрите http://www.bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html , там достаточно пространно объясняется, что такое зависимые типы и что на них можно сделать.

[zmila.livejournal.com]

а в pascal

type
  my_range = 1 .. 21;
  my_string = array [my_range] of char;
var
  my_i : my_range;
  my_s : my_string;

не то?

[thedeemon.livejournal.com]

Я показывал примеры, как на языке с упрощенными зависимыми типами это легко делается
http://thedeemon.livejournal.com/41035.html