November 27th, 2007

with Cat The Cat

ab_pokoj написал.

with Cat The Cat

Получил письмо от коллеги.

Мы замеряли производительности моделей систем.

Есть моя модель вычислителя будущего, написанная на Хаскеле и есть модель другой версии вычислителя будущего, выполненная на SystemC коллегами из отдела HDL по архитектуре, разрабатываемой нашими учеными.

Компьютеры у нас примерно однотипные, почти у всех стоят Hyperthreaded Intel Pentium's частотой 3.2GHz.

В обоих случаях моделировалась система с 16 процессорами, архитектуры похожи, хотя и отличаются.

Модель на SystemC работает со скоростью 5000 тактов моделирования за 400 секунд (12.5 такта в секунду). Отключение статистики улучшает это время на 20 секунд.

Моя модель работает со скоростью 2400 тактов за 70 секунд (34.3 такта в секунду). Отключение логов уменьшает это время до 2.3 секунды.

Вот так.

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

Не рекомендую. ;)
with Cat The Cat

Копирайт - оружие правящего класса.

with Cat The Cat

Хвастливый пост я написал, теперь напишу умный.

Я уже как-то упоминал про Type Inference and Reconstruction for First Order Dependent Types, интересную диссертацию про вывод зависимых типов данных.

Собственно, там странице на пятнадцатой находится следующий пример:
taut 0 f = f
taut (n+1) f = taut n (f False) && taut n (f True)
Это проверка, что функция f от N аргументов представляет собой тавтологию, истинную везде функцию.

Тип ее, согласно диссертации, тип taut следующий: R(λf.f)(λn'.λp.λf.(p (f True))&&(p (f False))). R - это fold по натуральным числам, первый аргумент применяется к 0, второй аргумент - к (n+1).

Что меня беспокоит во всем этом - а как это можно автоматически объяснить неподготовленному человеку?

Например, как исправить код f = return, чтобы ghc не выдавал ошибку, можно только спросив у более опытного коллеги. Если, конечно, уже не привык к этому.

С зависимыми типами все еще сложнее: как автоматически объяснить, что тип taut :: R... эквивалентен taut :: ∀n:N.n→((Bool→)n→Bool)->Bool? А если особых случаев больше одного?

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