deniok | Entries tagged with fprog

Как известно композиция двух функторов является функтором, причем fmap для этой композиции - это композиция fmap'ов:

GHCi> (fmap . fmap) (^2) [Just 3,Just 5,Nothing]
[Just 9,Just 25,Nothing]

Левый fmap протаскивает свой аргумент (fmap (^2)) через конструкторы списка, а дальше оставшийся fmap протаскивает свой аргумент (^2) через конструкторы Maybe.

( а фолды? траверсы? аппликативы? монады?... )

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)

Часто парсеры пишут в виде, допускающем разбор неоднозначных грамматик

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, конечно, еще потребуется, но тут, надеюсь, все справятся.)

Приведите пример таких объявлений типа данных с конструктором данных T и сигнатуры функции f, что реализация

f (T x) = T x

проходила бы проверку типов, a

f x = x

нет.

Мы привыкли, что правая свертка (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.

Почему это происходит, и какие минимальные изменения можно в нее внести, чтобы восстановить утраченную работоспособность?

Заказал на Озоне книжку Саймона Марлоу "Параллельное и конкурентное программирование на языке Haskell", переведенную уважаемым Виталием Брагилевским. Для рачительных и экономных сообщаю, что покупка на сайте издательства ДМК Пресс обойдется несколько дешевле.

Вот отзыв замечательного Романа Чепляки, правда на английскую версию.

Хорошая хотя и простая задачка возникла в процессе проверки домашних заданий. Чем отличается поведение следующих двух функций, и в чем причина такого отличия:

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)

К вопросу о заселении ⊥ при включенном 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

К завтрашнему занятию задачку со звёздочкой сделал, а то некоторые больно умные последние 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],[]]

Crossposts: http://deni-ok.livejournal.com/51673.html

Эти ваши интернеты бурлят:

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. Или получив самостоятельно.

Crossposts: http://deni-ok.livejournal.com/51411.html

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

Пускай мы реализовали на Хаскелле лямбда-термы

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)

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

Crossposts: http://deni-ok.livejournal.com/51180.html

Возьмём терм

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)) уже типизируем?

Crossposts: http://deni-ok.livejournal.com/50446.html

Ян

oxij написал Жёсткое введение в зависимые типы на Агде. Не могу не пропиарить. Открывайте и изучайте, свиньи вы эдакие (кроме, конечно, девушек) (c) r_l

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

Crossposts: http://deni-ok.livejournal.com/49824.html

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

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

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

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

Crossposts: http://deni-ok.livejournal.com/49291.html

От теории множеств к теории типов. Хорошая вводная статья Майка Шульмана о том, почему именно теорию типов стоит положить в основания математики. Ну немножко философского характера, конечно, но тематика обязывает. Настоятельно рекомендую, спасибо

alexey_rom за ссылку.

Crossposts: http://deni-ok.livejournal.com/48304.html

Сделал в ру-Википедии статью про сабж. ~~Еле поспел к Рождеству.~~ Держите.

Crossposts: http://deni-ok.livejournal.com/47912.html

Поправил в ru-Википедии своё же описание понятия зависимости одного от другого, долгое время меня раздражавшее. Поправил на более аккуратное, основанное на PTS-подходе. Что-то больно формально вышло, но проще уже слишком много профанации. Держите, вобщем.

Crossposts: http://deni-ok.livejournal.com/47627.html

Как лучше делать сопоставление с образцом в языке с зависимыми типами?

Coq's inductive types are implemented using separate "match" and "fix" constructions, which allow for deep matching, mutual matching, etc. Similarly, Agda allows function definition by pattern matching with a separate termination checker. However, this approach is only justified semantically by translating it into eliminators, and it is hard to make sense of for higher inductive types. On the other hand, deep matching is very useful for functional programmers.

One potential solution to this problem is the approach used in Epigram, where there is a "pattern matching" syntax that is extensible rather than baked into the system. Any term whose type has "the form of an induction principle" can be used to justify a pattern-matching syntax. Thus, although each inductive definition comes with its defining induction principle, the user can prove their own new induction principles (such as for deep matching, mutual recursion, etc.) and then use those elimination rules with the same sort of pattern-matching syntax.

This may be especially nice for higher inductive types, where preliminary experiments suggest that there can be meaningful notions of "deep recursion" and "mutual recursion" in particular cases, but it seems difficult to give one general formulation of such principles.

Crossposts: http://deni-ok.livejournal.com/47486.html

В Агде есть полезный зависимый тип данных - финитные натуральные. ( Кто они такие? )

Как можно конструктивно доказать, что число 4 является полным квадратом некоторого натурального числа? Предъявив такое число n, для которого n * n = 4. ( И мы знаем это число... )

Profile

deniok

February 2022

S	M	T	W	T	F	S
		1	2	3	4	5
6	7	8	9	10	11	12
13	14	15	16	17	18	19
20	21	22	23	24	25	26
27	28

Syndicate

Page Summary

Ратный труд обертки-композитора
Minimal Incomplete Definition
Не допускайте потери неоднозначности
id да не id
Куда прячется ленивость и как ее оттуда достать?
Параллельное и конкурентное программирование на языке Haskell
Тонкости точной семантики сопоставления с образцом
Парадокс Рассела: реализация на Агде
А вот кому трехпараметрических типов
Об умножение
Трудности с простыми лямбда-калькуляторами
Нищета и беспомощность просто типизированной лямбды
Brutal [Meta]Introduction to Dependent Types in Agda
Система F
От теории множеств к теории типов
Просто типизированное лямбда-исчисление
Дошли руки до лямбда-куба
Цитата для памяти
От перемены мест слагаемых тип суммы удивляет вас
Обратная функция на Агде

Style Credit

Style: Cloudy Days for Ciel by carisma_sensei

Expand Cut Tags

No cut tags

Page generated Apr. 23rd, 2025 02:51 pm