Зависит от реализации компилятора. Причем здесь CL? Например SBCL много где может TI.

ты говоришь про contstraint propagation, который в CL является деталью реализации. а я про вывод типов при компиляции

а я про вывод типов при компиляции

А зачем оно нужно в CL?

Да и не надо, я просто демонстрирую окружающим ущербность твоей логики. Чтобы никто не дай бог не подумал, что ты всерьез это все пишешь.

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

Нет смысла откладывать проверку ошибок до исполнения.

А не откладывать - есть смысл? Какой? Чем полезнее неотложить, чем отложить?

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

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

Которая в значительной степени ортогональна к тому, динамической или статической является типизация.

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

Это уже мало общего имеет со статической типизацией.

то все прекрасно ложится на чуть более сложный ADT, я вообще проблем не вижу.

Положи мне на атд тип сортированного списка, лол. В динамике с ним проблем никаких нет.

ок

http://web.student.chalmers.se/groups/datx02-dtp/html/SortedList.html

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

Как показывает практика, тайпинференс нужен весьма редко, а часто - вообще вреден. В общем случае надо уметь выводить лямбды, локальные переменные, полиморфный аргумент (и то не всегда, например, для high-rank типов вывод полиморфного аргумента должен быть запрещен).

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

Это зависимые типы, а не АТД. Ну и да - в лиспе оно делается в 1 строчку.

я перемудрил, надо посмотреть на monotraversable как правильно делать.

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}

class ToList x a | x -> a where toList :: x -> [a] 
instance ToList [a] a where toList = id
instance ToList b a => ToList [b] a where toList = concatMap toList

data T a = forall x . ToList x a => T x
         | T0 a

instance ToList (T a) a where
   toList (T x)  = toList x
   toList (T0 a) = [a]

flatten' :: [T a] -> [a]
flatten' = concatMap toList

test0 = flatten' []
test1 = flatten' [T0 1]
test2 = flatten' [T0 1, T0 2]
test3 :: [Int]
test3 = flatten' [T [T0 1,T0 2]]
test4 :: [Int]
test4 = flatten' [T0 1, T [T0 1, T0 2]]
test5 :: [Int]
test5 = flatten' [T0 1, T [T [T0 1,T0 2], T [T0 1]]]
test6 :: [[Int]]
test6 = flatten' [T0 [1,2], T [ T [T0 [1,2]]]]

То есть по-твоему это нормально, когда в столь тривиальной задаче можно «перемудрить» и надо что-то где-то как-то смотреть, чтобы правильно сделать? И какой должен быть опыт программирования на хаскеле, чтобы знать, чтобы сразу понять, что тут «надо посмотреть на monotraversable как правильно делать»?

tst-flatten.hs:1:1:
    The function `main' is not defined in module `Main'

у меня чот не компилится.

я правильно понимаю что

 flatten' [1, 2, [2, 8, 9, [[[[[5]]]]] [3, 14]]] 

И это, у тебя там T0, это какбы чит. Так любой дурак может. Ты без T0 покажи.

неа, чтобы положить рядом два разных типа нужно будет их в existential какой-нибудь завернуть. Тут так же ещё одна задница, в том, что неясно что делать из типа [[[a]]] -> это или a или [a], поэтому T0 вылезло.

[[[a]]] -> это или a или [a]

[a]. Более того, flatten a = [a], если а - не список.

не хочу :) ну давай, если быстро получится, то сделаю.

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}

class ToList x a where toList :: x -> [a]
instance ToList [a] a where toList = id
instance ToList b a => ToList [b] a where toList = concatMap toList
instance ToList a a where toList a = [a]


data T a = forall x . ToList x a => T x

instance ToList (T a) a where
   toList (T x)  = toList x

flatten' :: [T a] -> [a]
flatten' = concatMap toList

test1,test2,test3,test4,test5 :: [Int]
test0 = flatten' []
test1 = flatten' [T (1::Int)]
test2 = flatten' [T (1::Int), T (2::Int)]
test3 = flatten' [T [1::Int,2]]
test4 = flatten' [T (1::Int), T [1::Int, 2]]
test5 = flatten' [T [[1::Int]]]

ладно.. тут есть косяк.

а с чего это [a], а не a? судя по описанию задачи должно быть a.

Оно не то что не тайпчекнется, а ты такой параметр не напишешь :)

Мейна нет можешь просто в ghci поглядеть

судя по описанию задачи должно быть a.

Чего это? По описанию задачи оно принимает список и возвращает сплюснутый список. Значит если a - не список, то [a] -> [a]

палю https://ghc.haskell.org/trac/ghc/wiki/OverloadedLists

Это разные задачи, такую я уже без динамики не осилю :)

nuff said ;)

Это читерство :)

Не типы то будут, но за квалификаторами, за которыми они сильно много бонусов не дадут.

Я не уверен, что ты правильно прочитал или понял слова «динамическая _реализация_». Динамической реализацией я называю возможность горячей замены кода, в том числе, с изменением сигнатуры функции или класса.

Я посчитал это опиской. Горячая замена кода к типизации отношения не имеет, какой бы хитрой она не была.

А возможность динамически типизировать статическая система типов не отнимает. В D есть opCall, ЕМНИП, - вообще мечта динамиста.

Горячая замена кода к типизации отношения не имеет

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

как ты на горячую заменишь функцию, у которой сигнатура изменилась?

Например, так же как в UNIX с файлами.

При замене функции он применяется в других только при их перекомпиляции.

Плюс команда revdep-rebuild позволяющая перекомпилировать всё, у чего поменялись зависимости (после чего получаем новый консистентный образ)

Я не уверен, что ты правильно прочитал или понял слова «динамическая _реализация_». Динамической реализацией я называю возможность горячей замены кода, в том числе, с изменением сигнатуры функции или класса.

И в чем проблема?

И в чем проблема?

Что мне скажет тайпчекер, когда я попытаюсь «обновить» функцию, задав ей другую сигнатуру?

ну например как выразить в такую функцию в типах

Как обычно — Dom -> Cod, где Dom это тип которым ты хочешь ограничить входные значения, RoseTree<A> там (умные конструкторы, все дела), или List<Any>, а Cod — результата, List<A>, видимо.

Например — http://rosettacode.org/wiki/Flatten_a_list.

Ещё можно Tree<nesting_level, A> сделать, но это будет статичный nesting_level в большинстве языков (и скорее всего не нужный).

Как обычно — Dom -> Cod, где Dom это тип которым ты хочешь ограничить входные значения

Прямо капитан очевидность ворвался, лол. Только проблемка в том, что тип не выражается.

Что мне скажет тайпчекер, когда я попытаюсь «обновить» функцию, задав ей другую сигнатуру

Потребует обновить также все функции, где используется эта.

Вообще математически (в теории типов) не выражается или что?

Вот есть http://hackage.haskell.org/package/containers/docs/Data-Tree.html#v:flatten

flatten :: Tree a -> [a]

что тебе ещё нужно? Ничего кроме дерева ты не сконструируешь и в функцию не передашь, ничего кроме плоского списка правильных листов в нужном порядке (при правильной реализации) из функции не вылетит.

Потребует обновить также все функции, где используется эта.

То есть он не даст обновить эту ф-ю, пока не обновлю другие? А другие на даст обновить пока не обновлю эту? Ок.

Вообще математически (в теории типов) не выражается или что?

В какой-нибудь теории типов определенно выражается, лол.

Вот есть http://hackage.haskell.org/package/containers/docs/Data-Tree.html#v:flatten

Это дерево.

что тебе ещё нужно?

Нужен список.

А у тебя нет тут ошибки. Функция strlen x по определению (которое неправильно в твоей голове, а само по себе валидная конструкция) возвращает функциюlength. И дальше справедливо требует инстанс. Компилятор должен угадывать, что ты задумал?

То есть он не даст обновить эту ф-ю, пока не обновлю другие? А другие на даст обновить пока не обновлю эту?

Варианта как минимум два:

1. Транзакции на обновление (см. rpm и прочие пакетные менеджеры). Для тотального Type Inference единственный вариант.

2. Проверяется только тело функции. Функция изменяется только явно. Аналогия: библиотеки в UNIX. Соответственно, функцию можно обновить на новую версию, остальные функции используют старую версию пока не перезагрузятся.

Компилятор должен угадывать, что ты задумал?

В общем случае должен. Точнее опечатка не должна приводить к корректной программе. Если это не машинные коды и не forth.

Могу напомнить про старый фортран. В программе должна была быть конструкция

DO 5 I=1,10

из-за опечатки было введено

DO 5 I=1.10

Компилятор трактовал строку как DO5I=1.10 — присваивание вместо цикла. Космический корабль не попал на орбиту Венеры.

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

по определению (которое неправильно в твоей голове, а само по себе валидная конструкция)

Вот поэтому Type inference вреден. Усложняет отладку, требует для каждого значения ровно один тип, приводит к излишнему многословию программы, не позволяет описать некоторые структуры.

Это дерево.

Конкретнее это рекурсивный ADT F(x) = x * List(F(x)) (rose tree с листами типа x, да) вместо F(x) = 1 + x * F(x) (плоский связный список элементов типа x).

Нужен список.

Вложенный, ну то есть то что нормальный люди называют деревом :)

Там было [[[...[a]...]]] -> [a] — я вижу полиморфизм по a, так что второе это явно обычный плоский связный список / динамический массив элементов типа a (вроде [a]/std::vector<A>/List[A] в Haskell/C++/Scala), а первое — какое-то дерево / «вложенный список» листов типа a (может с тегом глубины в типе*, о чём только и может сказать количество скобок — в Haskell/C++ на GADTs/шаблонах можно устроить).

Если двинуться в сторону подтипирования, то из [Dynamic]/std::vector<boost:any>/List[Any] в него же.

Если без top type, то [a] <: a. [a] -> [a] — такой тип a, что [a] — подтип a (top type, очевидно, подходит, кроме него — устроить какаю-то иерархию наследников от общего интерфейса, как в ООП).

Дальше, условно, [a] <: a, b ~ a, b !~ [a]. [a] ->  — нужно чтобы b разделял с a все подтипы кроме [a] (может на наследовании тоже можно вырулить).

*) Это статически тогда будет, иначе нужны динамические статические системы типов типо агды :)

list :: Tree [Int]
list = Node [] [
                Node [] [Node [1] []],
                Node [2] [],
                Node [] [
                         Node [] [ Node [3] [],Node [4] []],
                         Node [5] []
                        ],
                Node [] [Node [] [Node [] []]],
                Node [] [Node [] [Node [6] []]],
                Node [7] [],
                Node [8] [],
                Node [] []
                ]

с конструкторами типов не интересно, я хочу обычный список передать на вход функции.

я хочу обычный список передать

Обычный список чего? В Haskell это важно.

Компилятор должен угадывать, что ты задумал?

Не должен. А пытается. В этом и претензия к нему.

элементом списка может быть либо a, либо список из a произвольной вложенности.

Ну это уже нифига не статическая типизация. А во втором случае - и вовсе никакая не горячая замена.

Конкретнее это рекурсивный ADT F(x) = x * List(F(x))

Нет.Это (forall a. List a)

Вложенный, ну то есть то что нормальный люди называют деревом :)

Нет, вложенный список не имеет ничего общего с деревом.

а первое — какое-то дерево / «вложенный список» листов типа a

Никаких деревьев. Просто список с произвольным уровнем вложенности.

Ну а вообще сам факт того что написание flatten в статике - тема для докторского диссера, уже показателен.

либо a, либо список ...

Тогда уже обязательно должен быть конструктор.

Даже в более простом случае «либо число, либо строка» приходится data и конструкторы делать.

написание flatten в статике - тема для докторского диссера

Можно ссылку на диссер?

Ну это уже нифига не статическая типизация.

Чем вариант с транзакциями не статическая типизация? Всё статически. Все уже существующие функции проверяются с учётом изменяемых. Если ошибка, то транзакция отменяется. Кстати, в SQL вроде так и есть. Пачка ALTER TABLE в транзакции либо целиком отработают либо целиком откатятся. В качестве типов можешь считать FOREIGN KEY.