TWIMC

Feb. 10th, 2015 10:05 pm
deniok: (ухмыляюсь)
Plan Foldable или Plan List?
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: (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: (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: (lambda cube)
Тут вопрос возник (не в первый раз):
typeof λx.x x
Отвечаем, например, так
> :set -XRankNTypes
> let f = (\x -> x x) :: (forall a. a -> a) -> (forall a. a -> a)
> f id 42
42
Или так
> let f' = (\x -> x x) :: (forall a. a) -> (forall a. a)
> f' undefined
*** Exception: Prelude.undefined


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: (Default)
Сегодня на stackoverflow, отвечая на вопрос, Andreas Hammar привёл хорошие примеры. Сохраняю на будущее, как простые задачки для студентов
data    D a = D a
data    S a = S !a
newtype N a = N a

constD x (D y) = x
constS x (S y) = x
constN x (N y) = x
Какие из следующих вызовов завершат свою работу как Deep Thought, а какие как Earth?
D undefined `seq` 42
S undefined `seq` 42
N undefined `seq` 42
constD 42 undefined
constS 42 undefined
constN 42 undefined
deniok: (lambda cube)
Напоминаю, что очередная встреча SPbHUG, которую теперь зовут FProg, пройдёт в четверг, 12 июля в 19:00 в офисе компании Яндекс. Предполагается, что нашему вниманию будут предложены следующие доклады:
  • Jan Malakhovski Введение в Agda.
  • Evgeny Kotelnikov Зависимые типы в Haskell.
  • Andrey Vlasovskikh Команда spb-archlinux на ICFP Contest 2009.

Подробная информация и регистрация на странице встречи.
deniok: (Default)
Три задачки с экзамена, в порядке усложнения условия.

Написать замкнутый терм типа (a -> b) -> ((a -> b) -> b) -> b.

Написать замкнутый терм типа (a -> b) -> ((a -> b) -> b) -> b, которому нельзя приписать тип c -> (c -> b) -> b.

Написать замкнутый терм с наиболее общим типом (a -> b) -> ((a -> b) -> b) -> b.
deniok: (Default)
Напишите представителя класса типов Applicative, для которого выполнялись бы законы Identity и Homomorphism:
pure id <*> u = u
pure u <*> pure x = pure (u x)
но не выполнялся бы законы Composition и/или Interchange:
pure (.) <*> u <*> v <*> x = u <*> (v <*> x)
u <*> pure x = pure ($ x) <*> u


UPD. Ну и по ходу дела возникли бонусные вопросы: написать такого представителя, чтобы не выполнялся (a) только Composition; (b) только Interchange.
deniok: (Default)
Устно вычислите значения побочные эффекты выражений и проверьте результат в GHCi:
let x = print "first" in print "second"

let x = print "first" in x >> print "second"

(\x -> print "first") (print "second")

print "first" `seq` print "second"
(Значения тоже можете вычислить в качестве бонуса:)
deniok: (Default)
А с каких это пор у нас в Data.Monoid поселился такой оператор
infixr 6 <>

(<>) :: Monoid m => m -> m -> m
(<>) = mappend
и где это задокументировано?
deniok: (Default)
Отличное упражнение на свойства комбинатора неподвижной точки fix.

Докажите равенство
fix (f . g) = f (fix (g . f))
deniok: (lambda cube)
Свободная теорема - это содержательное тождество, которое следует из типа любой параметрически полиморфной функции в полиморфно типизированном лямбда-исчислении. В "простых" полиморфных системах (вроде System F) свободные теоремы выполняются безусловно. В более богатых системах, например, в Хаскелле, имеются некоторые ограничения, возникающие из-за наличия в языке примитивов неограниченной рекурсии fix и строго вычисления seq, подробности см. [Johann06].

Read more... )

PS. Ну и чтобы всё было в одном месте - автоматический генератор свободных теорем.
deniok: (Default)
Имеется тип
data Tree a = Nil | Branch (Tree a) a (Tree a)
Написать функцию
elemTree :: Eq a => a -> Tree a -> Bool
проверяющую наличие значения в дереве.

Первая приходящая в голову реализация не проходит следующий тест:

> let testTree n =  Branch (testTree n) n (testTree (n+1))
> 3 `elemTree` (testTree 1)
True


Код теста специально сливается с фоном, попробуйте сначала догадаться самостоятельно, в чём тут подвох.

WTF

Nov. 19th, 2011 05:58 pm
deniok: (Default)
из Control.Applicative (с) Conor McBride and Ross Paterson 2005
newtype Const a b = Const { getConst :: a }

instance Functor (Const m) where
    fmap _ (Const v) = Const v

instance Monoid m => Applicative (Const m) where
    pure _ = Const mempty
    Const f <*> Const v = Const (f `mappend` v)


из Data.Functor.Constant (c) Ross Paterson 2010
(transformers package)
import Control.Applicative -- Sic!

...

newtype Constant a b = Constant { getConstant :: a }

instance Functor (Constant a) where
    fmap f (Constant x) = Constant x

...

instance (Monoid a) => Applicative (Constant a) where
    pure _ = Constant mempty
    Constant x <*> Constant y = Constant (x `mappend` y)


UPD. Росс ответил в кафе, что it was an accident

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. 22nd, 2017 10:28 pm
Powered by Dreamwidth Studios