Типы и типы

[metaclass]

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

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

Comments

[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 , там достаточно пространно объясняется, что такое зависимые типы и что на них можно сделать.