Re[10]: [Зависимые типы] Объясните на пальцах.
От: VoidEx  
Дата: 19.08.09 19:42
Оценка:
Здравствуйте, VladD2, Вы писали:

VD>Здравствуйте, lomeo, Вы писали:


L>>Это уже type checker.


VD>Ерунду какую-то говоришь. Проверка типов есть в любом языке не зависимо от наличия в нем вывода типов.


Именно, поэтому переписываю код WolfHound'а на Си++
template <class A, class B, unsigned int n>
Vec<B, n> vmap(std::function<B (A)> f, Vec<A, n> const &)
{ ... }

Где тут вывод типов?
Вот если бы сигнатуры vmap не было, то был бы вывод. А при подстановке конкретных параметров — это уже type check, как правильно заметил lomeo
Re[11]: [Зависимые типы] Объясните на пальцах.
От: VladD2 Российская Империя www.nemerle.org
Дата: 19.08.09 21:56
Оценка: +1
Здравствуйте, VoidEx, Вы писали:

VD>>Ерунду какую-то говоришь. Проверка типов есть в любом языке не зависимо от наличия в нем вывода типов.


VE>Именно, поэтому переписываю код WolfHound'а на Си++

VE>
VE>template <class A, class B, unsigned int n>
VE>Vec<B, n> vmap(std::function<B (A)> f, Vec<A, n> const &)
VE>{ ... }
VE>

VE>Где тут вывод типов?

Где-то в недрах "...". Точнее, так как это шаблон, то его вообще нет. Набор токенов, есть набор токенов. Вывод типов начнется когда в шаблон раскроется и в "..." попадут реальные типы.

А вообще, в твоем ответе чувствуется что-то не адекватное. Или ты не понял о чем идет речь, или намеренно пытаешься превратить обсуждение в бессмысленную кашу.

VE>Вот если бы сигнатуры vmap не было, то был бы вывод. А при подстановке конкретных параметров — это уже type check, как правильно заметил lomeo


Прочти еще раз ветку со слов Вольфхаунда и ниже. Обрати внимание, на слова о выводе типов внутри тел методов.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Re[6]: [Зависимые типы] Объясните на пальцах.
От: VladD2 Российская Империя www.nemerle.org
Дата: 19.08.09 22:08
Оценка:
Здравствуйте, lomeo, Вы писали:

L>Вывод типов и ЗТ, кажется, несовместимы.


Только если вести речь о выводе сигнатур глобальных функций и типов. А уровне тел функций проблем быть не должно.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Re[9]: [Зависимые типы] Объясните на пальцах.
От: thesz Россия http://thesz.livejournal.com
Дата: 20.08.09 16:04
Оценка:
Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, WolfHound, Вы писали:


WH>>Ну если в твоем понимании вывод типов это исключительно вывод сигнатуры функции то нету. В такой постановки вопроса и в немерле вывода типов нету.

WH>>Но если посмотреть повнимательней то ты наверное заметишь что внутри функции не указано ни одного типа.

L>Это уже type checker.


L>А то так получится, что когда я в Яве пишу выражение, то и там вывод типов работает.


В Агде двунаправленная проверка. Как и в Кайенне.

Снизу вывод, сверху проверяльщик.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.