deniok: (ухмыляюсь)
Как известно композиция двух функторов является функтором, причем fmap для этой композиции - это композиция fmap'ов:
GHCi> (fmap . fmap) (^2) [Just 3,Just 5,Nothing]
[Just 9,Just 25,Nothing]
Левый fmap протаскивает свой аргумент (fmap (^2)) через конструкторы списка, а дальше оставшийся fmap протаскивает свой аргумент (^2) через конструкторы Maybe.

а фолды? траверсы? аппликативы? монады?... )
deniok: (ухмыляюсь)
data Id a = Id {runId :: a} deriving (Eq,Show)

instance Traversable Id where
  sequenceA (Id x) = pure Id <*> x
 
instance Functor Id where
  fmap = fmapDefault

instance Foldable Id where
  foldMap = foldMapDefault
Какие неожиданные эффекты будут сопровождать следующий вызов, и в чем их причина?
GHCi> traverse Just (Id 5)

deniok: (ухмыляюсь)
Часто парсеры пишут в виде, допускающем разбор неоднозначных грамматик
newtype Parser a = Parser { apply :: String -> [(a, String)] }
(Тип apply это не что иное, как стандартный ReadS.) Однако, начав таким образом, лучше быть консистентным, поддерживая эту возможность повсюду, например
parse :: Parser a -> String -> [a]
parse p = map fst . filter (null . snd) . apply p
Сделайте приведенный выше парсер представителем Applicative и Alternative, так чтобы обеспечить следующее поведение
> twoChars x = (\a b -> [a,b]) <$> char x <*> char x
> threeChars x = (\a b c -> [a,b,c]) <$> char x <*> char x <*> char x
> parse (some (twoChars '7') <|> some (threeChars '7')) "777777"
[["77","77","77"],["777","777"]]
(Парсер char, конечно, еще потребуется, но тут, надеюсь, все справятся.)
deniok: (ухмыляюсь)
Приведите пример таких объявлений типа данных с конструктором данных T и сигнатуры функции f, что реализация
f (T x) = T x
проходила бы проверку типов, a
f x = x
нет.
deniok: (пацифик)
Мы привыкли, что правая свертка (foldr) хорошо заточена для работы с бесконечными списками:
> let mapPlusPi = foldr (\x xs -> (x+pi):xs) []
> head $ mapPlusPi [1..]
4.141592653589793
К сожалению, иногда возникают неприятности. Вот функция, которая берет список и выкидывает из него элементы стоящие на нечетных местах:
> let evenOnly = snd . foldr (\x (os,es) -> (x:es,os)) ([],[])
> evenOnly [1..10]
[2,4,6,8,10]
Только вот на бесконечном списке она ведет себя неподобающе
> head $ evenOnly [1..]
Interrupted.
Почему это происходит, и какие минимальные изменения можно в нее внести, чтобы восстановить утраченную работоспособность?
deniok: (lambda cube)
Заказал на Озоне книжку Саймона Марлоу "Параллельное и конкурентное программирование на языке Haskell", переведенную уважаемым Виталием Брагилевским. Для рачительных и экономных сообщаю, что покупка на сайте издательства ДМК Пресс обойдется несколько дешевле.

Вот отзыв замечательного Романа Чепляки, правда на английскую версию.
deniok: (lambda cube)
Хорошая хотя и простая задачка возникла в процессе проверки домашних заданий. Чем отличается поведение следующих двух функций, и в чем причина такого отличия:
diff xs = do
    p <- zip xs (tail xs)
    return $ abs (fst p - snd p)

diff' xs = do
    p <- zip (tail xs) xs
    return $ abs (fst p - snd p)
deniok: (ухмыляюсь)
К вопросу о заселении ⊥ при включенном type-in-type. Делается прямой реализацией парадокса Рассела
{-# OPTIONS --type-in-type --without-K #-} 
module russell where

open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty

-- a model of set theory
data U : Set where
  set : (I : Set) → (I → U) → U

-- a set is regular if it doesn't contain itself
regular : U → Set
regular (set I f) = (i : I) → ¬ (f i ≡ set I f)

-- Russell's set: the set of all regular sets
R : U
R = set (Σ U regular) proj₁

-- R is not regular
R-nonreg : ¬ (regular R)
R-nonreg reg = reg (R , reg) refl

-- R is regular
R-reg : regular R
R-reg (x , reg) p = subst regular p reg (x , reg) p

-- contradiction
absurd : ⊥
absurd = R-nonreg R-reg
Взято отсюда:
http://www.reddit.com/r/compsci/comments/1a7g6q/a_question_on_set_classes_and_dependent_types/
http://article.gmane.org/gmane.comp.lang.agda/5002
http://hpaste.org/84029
deniok: (Default)


К завтрашнему занятию задачку со звёздочкой сделал, а то некоторые больно умные последние 15 минут практики бьют баклуши, решив всё заданное.

Введём следующий трёхпараметрический типовый оператор, инкапсулирующий композицию однопараметрических конструкторов типов:
newtype Compose f g x = Compose {getCompose :: f (g x)}
Каков кайнд этого конструктора типов? Приведите пример замкнутого типа, сконструированного с помощью Compose, и пример терма этого типа.

Определите функцию
ffmap h = getCompose . fmap h . Compose
и объясните её выведенный тип. Попробуйте осуществить вызов
> ffmap (+42) $ Just [1,2,3]
В чём причина ошибки?

Чтобы обеспечить работоспособность подобного вызова, сделайте тип Compose представителем класса типов Functor:
instance (Functor f, Functor g) => Functor (Compose f g) where
  fmap                =   ???
Проверьте работоспособность на примерах:
> ffmap (+42) $ Just [1,2,3]
Just [43,44,45]
> ffmap (+42) $ [Just 1,Just 2,Nothing]
[Just 43,Just 44,Nothing]


Сделайте тип Compose представителем класса типов Applicative:
instance (Applicative f, Applicative g) => Applicative (Compose f g) where
  pure               = ???
  (<*>)              = ???
Проверьте работоспособность на примерах:
> getCompose $ (+) <$> Compose [Just 1,Just 2] <*> Compose [Nothing,Just 40]
[Nothing,Just 41,Nothing,Just 42]
> getCompose $ (+) <$> Compose [Just 1,Just 2] <*> Compose [Just 30,Just 40]
[Just 31,Just 41,Just 32,Just 42]
> getCompose $ Compose [[(+1)],[(+2),(+3)]] <*> Compose [[10,20],[]]
[[11,21],[],[12,22,13,23],[]]


deniok: (Рыжий)
Эти ваши интернеты бурлят:

ru-marazm.livejournal.com/3591670.html

lj.rossia.org/users/tiphareth/1685303.html

Агда, кстати, на стороне внучки, 9 раз по 2 литра будет 9 * 2:
_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + (m * n)
Впрочем внучке стоило бы снять все вопросы, предоставив доказательство
*-commutative : ∀ m n → m * n ≡ n * m
Взяв его, например, из Data.Nat.Properties. Или получив самостоятельно.

deniok: (Default)
А вот, кстати, при проверке лямбда-калькуляторов, написанных студентами, возникла такая задачка.

Пускай мы реализовали на Хаскелле лямбда-термы
data Term = 
    Var String
  | App Term Term
  | Lam String Term        
проверку их альфа-эквивалентности (можно и точное совпадение, для наших целей не важно):
alphaEq :: Term -> Term -> Bool
и одношаговую бета-редукцию (нормальную, для определенности, хотя это тоже не важно):
reduce :: Term -> Term
В последнем случае при отсутствии редексов просто возвращается исходный терм.

Если мы теперь хотим реализовать многошаговую бета-редукцию до нормальной формы, мы можем итерировать, делая шаг редукции до тех пор, пока терм не перестанет меняться. Ну, например, так
reduceToNF :: Term -> [Term]
reduceToNF = unfoldr step where 
  step t = 
      let next = reduсe t in 
    if t `alphaEq` next 
    then Nothing 
    else Just (t, next)


Не видите ли вы червоточины в этой схеме?

deniok: (Default)
  Возьмём терм
pre = \m.m pf pz (\t f.t)
pf = \p f.f(p(\t f.f))(\s z.s(p(\t f.f) s z))
pz = \f.f(\s z.z)(\s z.z)
который работает в бестиповой лямбде предесессором для чисел Чёрча:
pre (\s z.s(s(s z))) ->> \s z.s(s z)
pre (\s z.s(s z)) ->> \s z.s z
pre (\s z.s z) ->> \s z.z
pre (\s z.z) ->> \s z.z
(Рассказывают, что идея подобного предесессора пришла в голову Клини, когда он находился под воздействием веселящего газа при удалении четырёх зубов мудрости.)

Предесессор этот типизируем в просто типизированной лямбде страшным и ужасным типом, который слишком бесчеловечен, чтобы приводить его здесь. Желающие могут find'n'replace точечку на стрелочку (->) и отдаться в руки GHCi. Также типизируемы все его аппликации к числам Чёрча, тип их (в отличие от) благообразен и приятен глазу, ибо ожидаем : (a -> a) -> a -> a.

Имея pre, хочется определить вычитание. Это легко делается в бестиповой системе
minus = \k l.l pre k
Работает ли такой подход в просто типизированной лямбде? На первый взгляд да, тип может быть приписан этому терму, желающие на него взглянуть опять-таки отсылаются в GHCi. К несчастью этот minus умеет, оставаясь типизированным, вычитать числа, не большие единицы. Скажем
minus (\s z.s(s(s z))) (\s z.s z) ->> \s z.s(s z)
ещё работает, обладая пристойным типом (a -> a) -> a -> a на всех 27 шагах редукции (счёт вёлся для нормальной стратегии). А вот вычитание из числа 3 числа 2 хоть и даёт 1 при редукциях, но не позволяет типизировать нередуцированный терм.
minus (\s z.s(s(s z))) (\s z.s(s z)) ->> \s z.s z
Кстати говоря, место где типизация волшебным образом возникает, находится почти в самом начале цепочки редукций. Из 43 шагов этого вычитания 40 последним может быть приписан тип (a -> a) -> a -> a, последний нетипизируемый терм
(\s z.s(s z)) pre (\s z.s(s(s z))) 
а следующий в редукционной цепочке
(\z.pre (pre z)) (\s z.s(s(s z))) 
уже согласен приписать себе обычный числовой тип.

Может кто-нибудь, кстати, придумать более простой, чем предесессор Клини, терм, обладающий таким же свойством: (\s z.s(s z)) term не имеет типа, а единожды редуцированный (\z.term (term z)) уже типизируем?

 
deniok: (typed lambda)
 Ян [livejournal.com profile] oxij  написал Жёсткое введение в зависимые типы на Агде. Не могу не пропиарить. Открывайте и изучайте, свиньи вы эдакие (кроме, конечно, девушек) (c) r_l

UPD: обсуждение в Твиттере

deniok: (typed lambda)
Обогатил ру-Википедию стать ей про это дело. Ловите. Надо бы ещё, конечно, понаписать про точное определение и всякие свойства, но пока лень.

UPD: Понаписал про формальности.

UPD2: Добавил типизацию по Карри с классическим примером, демонстрирующим, что System F богаче просто-типа-лямбды. И готовящим читателя к рассуждениям про импредикативность и ограниченные версии System F.

UPD3: Уф. Доделал-таки.

deniok: (Default)
От теории множеств к теории типов. Хорошая вводная статья Майка Шульмана о том, почему именно теорию типов стоит положить в основания математики. Ну немножко философского характера, конечно, но тематика обязывает. Настоятельно рекомендую, спасибо [livejournal.com profile] alexey_rom за ссылку.

deniok: (Default)
Сделал в ру-Википедии статью про сабж. Еле поспел к Рождеству.  Держите.
deniok: (lambda cube)
Поправил в ru-Википедии своё же описание понятия зависимости одного от другого, долгое время меня раздражавшее. Поправил на более аккуратное, основанное на PTS-подходе. Что-то больно формально вышло, но проще уже слишком много профанации. Держите, вобщем.
deniok: (ухмыляюсь)
Как можно конструктивно доказать, что число 4 является полным квадратом некоторого натурального числа? Предъявив такое число n, для которого n * n = 4. И мы знаем это число... )

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 24th, 2017 03:01 am
Powered by Dreamwidth Studios