Recycled Bin
03 Март 2008 @ 11:08
INC
0x20
16 пнуло | пнуть
25 Февраль 2008 @ 18:14
об абстрагировании
Хаскель предлагает достаточно удобный для большинства задач уровень абстракции - алгебраические типы, сравнение с образцом, классы типов. Забираясь выше, легко попасть в ловушку не решения проблемы предметной области, не достижения цели, а решения проблемы отображения решения проблемы предметной области на фиксированный уровень абстракции и ни ангстремом ниже.
Здесь (
22 Февраль 2008 @ 21:40
ЙО!
07 Февраль 2008 @ 16:32
Лем живее всех живых
Трурль и Клапауций опять спорят. Теперь уже о том, что называть функциональным языком.
27 Январь 2008 @ 01:32
typechecker для dependent types system
Заинтересовал меня всё таки
kurilka тотальным ФП, а у
deni_ok и
thesz я понахватался ссылок и умных слов. Ну, ещё и dependent types в стороне не остались.
Подумал, что total fp будет неплохо смотреться для программирования на типах - гарантия завершения будет тут очень кстати.
К сожалению, "по семейным обстоятельствам" я сейчас не в силах заняться чем нибудь серьёзно, поэтому всё, что я здесь пишу - скорее для себя, чтобы не забыть. Написано очень нудно (это тоже для себя, извините - я тупой) и сумбурно (а это так получилось).
Итак что здесь? (чтобы вы решили читать или нет)
Здесь размышления о том, как должен работать тайпчекер в системе с зависимыми типами. Я пытаюсь придумать приёмы, позволяющие строить гарантировано завершающиеся доказательства/опровержения.
( Итак, о чём думал, пока ужинал макаронами. )
Если у кого то есть материалы по теме, накидайте сюда плз - потом как руки дойдут обязательно прочту всё-всё-всё :-)
Подумал, что total fp будет неплохо смотреться для программирования на типах - гарантия завершения будет тут очень кстати.
К сожалению, "по семейным обстоятельствам" я сейчас не в силах заняться чем нибудь серьёзно, поэтому всё, что я здесь пишу - скорее для себя, чтобы не забыть. Написано очень нудно (это тоже для себя, извините - я тупой) и сумбурно (а это так получилось).
Итак что здесь? (чтобы вы решили читать или нет)
Здесь размышления о том, как должен работать тайпчекер в системе с зависимыми типами. Я пытаюсь придумать приёмы, позволяющие строить гарантировано завершающиеся доказательства/опровержения.
( Итак, о чём думал, пока ужинал макаронами. )
Если у кого то есть материалы по теме, накидайте сюда плз - потом как руки дойдут обязательно прочту всё-всё-всё :-)
23 Январь 2008 @ 13:50
kind функционального типа
18 Январь 2008 @ 13:04
Дезинтегратор
13 Декабрь 2007 @ 11:45
почему я не хожу на выборы
06 Декабрь 2007 @ 14:57
Не могу доказать :-(
Небольшое вступление.
Есть такой модуль Control.Applicative, в котором определён класс Applicative
т.е. он чуть шире
( тут мне непонятно )
Есть такой модуль Control.Applicative, в котором определён класс Applicative
class Functor a => Applicative a where
pure :: a -> f a
<*> :: f (a -> b) -> f a -> f b
т.е. он чуть шире
Functor (за счёт pure), и чуть уже Monad. Золотая середина - полезно, когда нам от монад нужен только return.( тут мне непонятно )
06 Ноябрь 2007 @ 12:49
FYI I am a spy ;-)
Давно ничего не писал, обновлю журнал.
Вот парень классно прикололся.
Пробежал позавчера HL2E2. Атака страйдеров отражается так - убиваешь охотников машиной, при этом у тебя скорее всего будут тяжёлые потери, но охотник валится сразу; либо гравипушкой закидываешь их какашками - так ты более мобилен и сил для игр и роста остаётся гораздо гораздее. Дальше просто - бомбу-липучку к пузу и биг-бада-бум!! Ах да! Ещё я бомб вокруг себя побросал, чтобы их не ждать в телепорте.
Вот парень классно прикололся.
Пробежал позавчера HL2E2. Атака страйдеров отражается так - убиваешь охотников машиной, при этом у тебя скорее всего будут тяжёлые потери, но охотник валится сразу; либо гравипушкой закидываешь их какашками - так ты более мобилен и сил для игр и роста остаётся гораздо гораздее. Дальше просто - бомбу-липучку к пузу и биг-бада-бум!! Ах да! Ещё я бомб вокруг себя побросал, чтобы их не ждать в телепорте.
15 Октябрь 2007 @ 14:47
Горилла в чувствах-с
12 Июль 2007 @ 12:51
Опять про Monadability
04 Июль 2007 @ 18:57
Кстати!
Для equational reasoning в Haskell можно (иногда нужно) пользоваться GHC Rules (На Haskellwiki), чтобы написанное было читабельным и maintainable, а скомпилированное эффективным. А для нахождения нужных правил можно воспользоваться Theorem for Free. Например, его автоматической выводилкой. Или использовать free / ft команды lambdabot-а.
К сожалению, что нибудь более-менее автоматического для типов, отличных от стандартных, я найти не могу. Остаётся или выводить правила руками, или строить по аналогии со стандартными, а затем проверять на корректность.
Это я всё мечтаю. Нарисовал нужные типы данных, сформировал по ним типы функций для работы над ними, автоматически построил их реализацию, автоматически построил правила, выбрал нужные для оптимизации. А дальше работаешь легко и непринуждённо. Это идеал, разумеется. Но я уверен, что частично эту работу можно автоматизировать. Типа того, что при доказательстве Coq'ом ему надо указывать стратегии, так же и здесь при реализации тела функции надо направлять "думатель".
Это вообще возможно? А то у меня каша в голове.
К сожалению, что нибудь более-менее автоматического для типов, отличных от стандартных, я найти не могу. Остаётся или выводить правила руками, или строить по аналогии со стандартными, а затем проверять на корректность.
Это я всё мечтаю. Нарисовал нужные типы данных, сформировал по ним типы функций для работы над ними, автоматически построил их реализацию, автоматически построил правила, выбрал нужные для оптимизации. А дальше работаешь легко и непринуждённо. Это идеал, разумеется. Но я уверен, что частично эту работу можно автоматизировать. Типа того, что при доказательстве Coq'ом ему надо указывать стратегии, так же и здесь при реализации тела функции надо направлять "думатель".
Это вообще возможно? А то у меня каша в голове.
26 Июнь 2007 @ 17:29
Токипона: ссылки
Официальный сайт токипоны.
Уроки токипоны:
[RUS]Токипона на wikibooks (переведённые от jan Pije). Классика. Учитесь по этим урокам.
[RUS]Уроки от jan Lekalo. Это даже не уроки. Парень учит токипону и по ходу обучения рассказывает про неё. По моему первый обучающий ресурс на русском.
[RUS]Уроки на лингвисто от jan Eliki. Неоконченные, но проникнутые духом токипоны. Есть красивая азбука от Lament.
Общества, группы и т.д.
WIKI на TP.
TP на LJ.
[RUS]TP на русском LJ.
TP группа на yahoo.
Персональные странички
jan Pije. Тексты, картинки, музыка. Есть сценарий "В поисках священного Грааля" Монти Пайтона.
jan Jakopo. Частота употребления звуков. Панграммы.
jan Ke. Гимны, молитвы.
Потом допишу, неохота вспомнить.
Письменность
Тенгвар
Скоропись или что то вроде этого. Не помню.
Хангыл. Самое симпатичное по мне. Сэмпл.
Иероглифы. Прикольно.









Иероглифы неоконченное
Послушать, посмотреть
shinan с 9:22 до 13:41 прикольно так болтает.
Песенки от Pije
Ещё где то лежало "mama pi mi mute o". Что то не найду сходу.
Уроки токипоны:
[RUS]Токипона на wikibooks (переведённые от jan Pije). Классика. Учитесь по этим урокам.
[RUS]Уроки от jan Lekalo. Это даже не уроки. Парень учит токипону и по ходу обучения рассказывает про неё. По моему первый обучающий ресурс на русском.
[RUS]Уроки на лингвисто от jan Eliki. Неоконченные, но проникнутые духом токипоны. Есть красивая азбука от Lament.
Общества, группы и т.д.
WIKI на TP.
TP на LJ.
[RUS]TP на русском LJ.
TP группа на yahoo.
Персональные странички
jan Pije. Тексты, картинки, музыка. Есть сценарий "В поисках священного Грааля" Монти Пайтона.
jan Jakopo. Частота употребления звуков. Панграммы.
jan Ke. Гимны, молитвы.
Потом допишу, неохота вспомнить.
Письменность
Тенгвар
Скоропись или что то вроде этого. Не помню.
Хангыл. Самое симпатичное по мне. Сэмпл.
Иероглифы. Прикольно.










Иероглифы неоконченное
Послушать, посмотреть
Песенки от Pije
Ещё где то лежало "mama pi mi mute o". Что то не найду сходу.
25 Июнь 2007 @ 13:05
mi jo e jan lili
22 Июнь 2007 @ 10:43
18 Июнь 2007 @ 17:13
Опять про паттерн матчинг
На RSDN технические работы.
( Read more... )
P.S. А ещё я сегодня видел в метро парня, читавшего распечатку "Знакомство с языком Haskell" или что то в этом духе ;-)
P.P.S. А ещё я подумал, что изобрёл слово "индексикация" как перевод indexitis (болезнь использования (!!) в Haskell), а оно оказывается существует реально и означает совсем-совсем другое :-(
( Read more... )
P.S. А ещё я сегодня видел в метро парня, читавшего распечатку "Знакомство с языком Haskell" или что то в этом духе ;-)
P.P.S. А ещё я подумал, что изобрёл слово "индексикация" как перевод indexitis (болезнь использования (!!) в Haskell), а оно оказывается существует реально и означает совсем-совсем другое :-(
08 Июнь 2007 @ 17:23
Про лямбду, как всегда.
21 Май 2007 @ 15:58
Задачка со свёрткой
Читал статью Bernie Pope "Getting a Fix from the Right Fold" из The Monad. Reader Issue 6. В ней решается задачка о написании
У меня удивительно быстро получилось решить эту задачку. Решение было эквивалентным решению 2 в статье.
( Подглядеть )
dropWhile через foldr. В частности, эта задачка решалась в Graham Hutton "A Tutorial on the Universality and Expressiveness of Fold" через таплы.У меня удивительно быстро получилось решить эту задачку. Решение было эквивалентным решению 2 в статье.
( Подглядеть )