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: (ухмыляюсь)
В стандартной библиотеке (Data.Foldable) имеется функция
> :t asum
asum :: (Alternative f, Foldable t) => t (f a) -> f a
> asum [Nothing, Just 1, Just 2]
Just 1
> asum [[1,2,3],[4,5]]
[1,2,3,4,5]
Можете ли вы написать afold с естественной для своего типа семантикой:
> :t afold
afold :: (Alternative f, Foldable t) => t a -> f a
>  afold "abc" :: Maybe Char
Just 'a'
>  afold "abc" :: [Char]
"abc"
Я знаю три решения: кривое (требующее FlexibleInstances и IncoherentInstances), обычное (утилизирующее избыточно богатый интерфейс Foldable) и современное, элегантно выпрямляющее кривизну кривого.
deniok: (ухмыляюсь)
... и педантично выровнял:
($)    ::                      (a -> b) ->   a ->   b
(<$>)  :: Functor     f  =>    (a -> b) -> f a -> f b
(<*>)  :: Applicative f  =>  f (a -> b) -> f a -> f b
(=<<)  :: Monad       m  =>  (a -> m b) -> m a -> m b

(&)    ::                      a ->   (a -> b) ->   b  -- Data.Function
(<&>)  :: Functor     f  =>  f a ->   (a -> b) -> f b  -- Control.Lens.Operators
(<**>) :: Applicative f  =>  f a -> f (a -> b) -> f b  -- Control.Applicative
(>>=)  :: Monad       m  =>  m a -> (a -> m b) -> m b
deniok: (ухмыляюсь)
Приведите пример таких объявлений типа данных с конструктором данных T и сигнатуры функции f, что реализация
f (T x) = T x
проходила бы проверку типов, a
f x = x
нет.
deniok: (Рыжий)
Размышляю тут вторые сутки над вопросом, что делает контекст Foldable в определении класса типов Traversable
class (Functor t, Foldable t) => Traversable t where
  ...
Технически он не нужен: никакая функциональность Foldable не используется ни при выражении законов Traversable, ни для реализации по умолчанию его методов.

Контекст Functor, кстати, не вызывает вопросов в техническом отношении: он нужен и для формулировки законов (Naturality и Composition для sequenceA и Composition для traverse) и для реализации по умолчанию
traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
traverse f = sequenceA . fmap f

Соображения, которыми руководствовались разработчики класса типов Traversable, включая контекст Foldable, заключаются в довольно разумном соображении: любой Traversable является Foldable в том смысле, что имея traverse можно гарантированно и универсально реализовать Foldable с помощью нехитрой машинерии:
foldMap :: (Traversable t, Monoid m) => (a -> m) -> t a -> m
foldMap f = getConst . traverse (Const . f)
(эта функция присутствует в Data.Traversable под именем foldMapDefault).

Тем не менее решение о "наследовании" Traversable от Foldable имеет свою цену. Теперь, объявляя некоторый тип MyType представителем Traversable, я должен сначала сделать его представителем Foldable. Даже если я совсем не собираюсь пользоваться Foldable-интерфейсом, я должен написать затычку
instance Foldable MyType where
    foldMap = foldMapDefault
Это не очень большая цена, но представим, что через пару лет ресерчеры обнаружат, что есть замечательный класс типов SomethingInterestingAndTrendyable и что с помощью traverse можно реализовать его единственную ключевую функцию somethingInterestingAndTrendyImpl. То есть Traversable является (is a :)
SomethingInterestingAndTrendyable и поэтому нужно сделать
class (Functor t, Foldable t, SomethingInterestingAndTrendyable t) => Traversable t where
  ...
а для "удобства" добавить somethingInterestingAndTrendyImplDefault. Не думаю, что мы будем этим очень довольны, хотя технически в каждый наш инстанс Traversable потребуется добавить лишь
instance SomethingInterestingAndTrendyable MyType where
    somethingInterestingAndTrendyImpl = somethingInterestingAndTrendyImplDefault


Но раз уж мы двинулись по этому пути "проявленных наследований" (а мы таки двинулись, см. Monad и Applicative), почему бы не переложить эту деятельность на компилятор? Вроде есть напрашивающееся решение: разрешить в Хаскелле в классах-наследниках задавать методы по умолчанию для классов-родителей. То есть вместо внешней по отношению к классу foldMapDefault и ей подобных разрешить писать
class (Functor t, Foldable t, SomethingInterestingAndTrendyable t) => Traversable t where
    -- default impls for Traversable methods
    traverse = ...
    -- default impls for parents methods
    fmap f = getId . traverse (Id . f)
    foldMap f = getConst . traverse (Const . f)
    somethingInterestingAndTrendyImpl = ...
В этом случае словари для родительских классов могут при необходимости генерироваться автоматически (если у нас достаточно реализаций по умолчанию), и разработчики будут освобождены от написания фейковых родительских инстансов.

Discuss.

UPD. В комментах сказали, что proposal такой имеется. Нашел, https://wiki.haskell.org/Class_system_extension_proposal, почитал. Мрак. C++ как мы его знаем, практически все прелести разрешения коллизий при множественном наследовании реализации. Нам такого не надо. Вывод: наследование - зло, его надо избегать, долой контекст Foldable из Traversable (и, как мне тут подсказывают, Applicative из Monad).
deniok: (Рыжий)
GHC 7.10.1 :
class Applicative m => Monad m where
...
    return      :: a -> m a
    return      = pure
...
-- оставили как было (по социальным причинам :)
--  (>>) :: forall a b. m a -> m b -> m b
--  (>>) = (*>)
...
https://hackage.haskell.org/package/base-4.8.0.0/candidate/docs/src/GHC-Base.html#Monad
deniok: (typed lambda)
Циклическую ротацию списка влево
> rotate 3 [1..10]
[4,5,6,7,8,9,10,1,2,3]
легко определить, используя take и drop:
> let rotate n xs = drop n xs ++ take n xs
Если напустить на это дело pointfree, он даст безумное:
rotate = ap (ap . ((++) .) . drop) take


Можете ли вы написать полностью бесточечную реализацию rotate, сцепив take и drop ровно одной стандартной библиотечной функцией?
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)
А вот, кстати, что у нас в CS Клубе будет в конце сентября. Джон Хариссон прочитает 5 лекций про автоматическое доказательство теорем. Я считаю, что это замечательно.
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: (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: (typed lambda)
 Ян [livejournal.com profile] oxij  написал Жёсткое введение в зависимые типы на Агде. Не могу не пропиарить. Открывайте и изучайте, свиньи вы эдакие (кроме, конечно, девушек) (c) r_l

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

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 Jul. 25th, 2017 02:51 pm
Powered by Dreamwidth Studios