deniok: (Default)

(1) Является ли отношение многошаговой бета-редукции на термах бестипового лямбда-исчисления отношением порядка? Докажите или приведите контрпример.

(2) Верен ли ваш ответ для просто типизированной лямбды?

про ЖЖ

Apr. 4th, 2017 09:50 am
deniok: (Default)
Не читал (дальше первого абзаца) и не подписывал ТОС. Путин и Медведев должны уйти в отставку, после всего, что наворотили за последние 5 лет, а репрессивное законодательство отменено, чем скорее тем лучше. Писать здесь (в ЖЖ) не буду и транслировать тоже, через некоторое время журнал удалю. Образовательный и прочий контент из ЖЖ скопирован на dreamwidth.org. Всем привет.
deniok: (Default)
Инхабитация fmap для монад Cont и Sel - мой любимый дополнительный вопрос на экзамене. Справитесь?
? :: (a -> b) -> ((a -> r) -> r) -> ((b -> r) -> r)
? :: (a -> b) -> ((a -> r) -> a) -> ((b -> r) -> b)
Чтобы помучить студентов посильнее я предлагаю проинхабитировать (<*>) для Cont:
? :: (((a -> b) -> r) -> r) -> ((a -> r) -> r) -> ((b -> r) -> r)
А вот (<*>) для Sel я студентам на экзаменах не даю. Может стоило бы?
? :: (((a -> b) -> r) -> (a -> b)) -> ((a -> r) -> a) -> ((b -> r) -> b)
(Те, кто вызывает джинна, заведомо считаются проигравшими.)
deniok: (Default)
Мнения просвещенных твиттерян разделились поровну. Соперники идут ноздря в ноздрю. Присоединяйтесь, кто еще не.
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: (ухмыляюсь)
Originally posted by [livejournal.com profile] edwardahirsch at Предвыборное
Если что, в воскресенье я собираюсь придти и проголосовать за Яблоко и яблочных депутатов всеми четырьмя бюллетенями.

Начало федерального списка у них неплохое, и никакой агитации за других разумных кандидатов я не видел. Ну, и вообще, яблочный год и время собирать камни.

Чего и вам желаю.
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: (ухмыляюсь)
Все-таки оставили:
GHCi> :i ($)
($) ::
  forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
  (a -> b) -> a -> b
        -- Defined in `GHC.Base'
infixr 0 $
GHCi> :i undefined
undefined ::
  forall (r :: GHC.Types.RuntimeRep) (a :: TYPE r).
  GHC.Stack.Types.HasCallStack =>
  a
        -- Defined in `GHC.Err'
Хорошо хоть
> :t ($)
($) :: (a -> b) -> a -> b
> :t undefined
undefined :: a
deniok: (ухмыляюсь)
В выражении
GHCi> succ <$> "abc"
"bcd"
оператор <$> имеет тип (Char -> Char) -> [Char] -> [Char]. Верно ли это утверждение для обоих вхождений <$> в следующем выражении
GHCi> succ <$> succ <$> "abc"
"cde"
deniok: (ухмыляюсь)
Приведите пример таких объявлений типа данных с конструктором данных T и сигнатуры функции f, что реализация
f (T x) = T x
проходила бы проверку типов, a
f x = x
нет.
deniok: (ухмыляюсь)
Померил тут, похоже про магические хэши не надо рассказывать. Тут length' - текущая реализация из GHC, length0 - трех?летней давности:
{-# LANGUAGE MagicHash #-}
module Length where

import GHC.Prim
import GHC.Exts (Int(I#))
import Data.List

length0    :: [a] -> Int
length0 l  =  len l 0#
  where
    len           :: [a] -> Int# -> Int
    len []     a# =  I# a#
    len (_:xs) a# =  len xs (a# +# 1#)

length' :: [a] -> Int
length' xs = lenAcc xs 0 where
  lenAcc []     n = n
  lenAcc (_:ys) n = lenAcc ys (n+1)

length'' :: [a] -> Int
length'' = foldl' (const . succ) 0

length''' :: [a] -> Int
length''' []     = 0
length''' (_:xs) = 1 + length''' xs
Результаты
C:\Users\deniok\Documents\Haskell>ghc -O2 Length.hs
[1 of 1] Compiling Length           ( Length.hs, Length.o )

C:\Users\deniok\Documents\Haskell>ghci Length.hs
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
Ok, modules loaded: Length.
> :set +s
> length [1..100000000]
100000000
(1.56 secs, 8,014,793,624 bytes)
> length0 [1..100000000]
100000000
(1.55 secs, 8,002,029,776 bytes)
> length' [1..100000000]
100000000
(1.55 secs, 8,001,085,992 bytes)
> length'' [1..100000000]
100000000
(2.00 secs, 9,601,216,960 bytes)
> length''' [1..100000000]
*** Exception: stack overflow
>
> length [1..50000000]
50000000
(0.86 secs, 3,938,034,240 bytes)
> length0 [1..50000000]
50000000
(0.84 secs, 3,937,631,120 bytes)
> length' [1..50000000]
50000000
(0.84 secs, 4,240,225,000 bytes)
> length'' [1..50000000]
50000000
(1.08 secs, 4,845,463,912 bytes)
> length''' [1..50000000]
50000000
(1.34 secs, 4,420,898,928 bytes)
deniok: (Рыжий)
Между Haskell Report и GHC base имеется дивная взаимная рекурсия.

В GHC base мы имеем такое определение наименьшей неподвижной точки (least fixpoint)
fix :: (a -> a) -> a
fix f = let x = f x in x

В Haskell Report в разделе 3.12 описана трансляция для выражения let в ядро (привожу только релевантные правила)
...
let p = e1 in e0    =    case e1 of ˜p -> e0
                             where no variable in p appears free in e1
let p = e1 in e0    =    let p = fix (\˜p -> e1) in e0
с замечанием "where fix is the least fixpoint operator".

Чтобы понять рекурсию, нужно понять рекурсию.
deniok: (Рыжий)

Кубик Рубика мы активно крутили в девятом классе средней школы, то есть в 1982 году. С тех пор у меня осталась куча листочков с записями разных алгоритмов.

Спустя 17 лет, в 1999 году, я обнаружил эти листочки в горе мусора, предполагавшегося к отправлению на помойку. Тогда я решил, что стоит перенести все это знание в более долговечный и удобный в использовании формат. На дворе как раз заканчивал надуваться первый интернет-пузырь, доткомы рвались в заоблачную высь, и я решил убить нескольких зайцев одним махом. А именно, изучить Джаву, оформить все алгоритмы в виде джава-апплетов с крутящимися кубиками, забацать сайт и выложить его в глобальную сеть. Что и было успешно проделано.

Прошло еще 17 лет. Сегодня [livejournal.com profile] ivan_gandhi упомянул полоску/змейку на кубике Рубика, и я залез на deniok.narod.ru, куда все это было выложено, скопировать картинку варианта змейки. И обнаружил, что в современном мире джава-апплеты уже практически не работают. Единственный браузер в котором мне удалось заставить все крутиться - Firefox (c AdBlock'ом, конечно, иначе на народе реклама вытесняет все содержательное в дальний угол). Но и там, вроде, апплетам недолго осталось жить. Я, правда, все-таки был достаточно умен, чтобы закодировать алгоритм, который должен проигрываться на кубике, в виде параметров апплета. Типа param name="pAlgToApply" value="0,-9,8,9,-8,0,0". То есть извлечь содержательную информацию из html можно. Но тем не менее.

А листочки с алгоритмами до сих пор целы.

Разумный человек коль баснь сию прочтет, то, верно, и мораль из оной извлечет.

deniok: (ухмыляюсь)
А вот скажите, пожалуйста, та идея что присваивание полю структуры может менять не только значение, но и тип структуры, она помимо кметтовских линз где-нибудь еще в статически типизированных языках реализована?
> ('z', True) & _1 .~ 42
(42, True)


UPD. Мне тут делают совершенно резонное замечание, что стандартный синтаксис модификации записей в Хаскеле обладает этим свойством:
> data Pair a b = Pair {fstP :: a, sndP :: b} deriving Show
> let p1 = Pair True 'z'
> :t p1
p1 :: Pair Bool Char
> let p2 = p1 {fstP = 42}
> :t p2
p2 :: Num a => Pair a Char
У меня это совершенно вылетело из головы.
deniok: (Рыжий)
Маленький хаскеллист попал в Зазеркалье и, преодолев неисчислимые препятствия, дошел до последней горизонтали. Белая и Черная Королевы говорят, что для того, чтобы стать SPJ, ему нужно пройти «Королевский экзамен», ответив на Черный и Белый вопросы: всякий ли Functor является Rotcnuf? всякий ли Rotcnuf является Functor?
class Rotcnuf f where
  mfap :: f (a -> b) -> a -> f b

Помогите маленькому хаскеллисту стать SPJ.
deniok: (Рыжий)
А вот Category Theory by Steve Awodey - хороший же вводный курс для магистров и продвинутых бакалавров IT/CS. Автор учился у МакЛейна в Чикаго, потом десять лет читал в Carnegie Mellon, причем не только для математиков, но и для студентов в Computer Science, Logic, Linguistics, Cognitive Science, Philosophy. По мне так просто бери мел и читай, все уже продумано.

Есть какие-то другие мнения?
deniok: (Рыжий)
Как вам скорее всего известно, написать представителя класса типов Functor для типа эндоморфизма невозможно. Если неизвестно, то можете попробовать
newtype Endo a = Endo (a -> a)

instance Functor Endo where
   fmap f (Endo g) = Endo undefined
Даже если ваш результат сойдется по типам, законам для функтора он удовлетворять не будет.

Вот вам другой экспоненциальный тип данных, для которого, однако, написать законного представителя класса типов Functor можно:
newtype Quest b a = Quest ((a -> b) -> a)

instance Functor (Quest b) where
  fmap f (Quest g) = Quest undefined
Попробуйте сделать это, после чего ответьте на вопрос: чему равен результат такого вызова
> let Quest f = fmap succ $ Quest (\h -> h 40) in f id

Profile

deniok: (Default)
deniok

September 2017

S M T W T F S
     12
3456789
10111213141516
17181920212223
24252627282930

Syndicate

RSS Atom

Style Credit

Expand Cut Tags

No cut tags
Page generated Oct. 17th, 2017 11:55 pm
Powered by Dreamwidth Studios