Ага, свежачок

@bravit111 на курсах про идрис я спрашивал, про то можно ли с уникальными типами сортировку больее-менее доказанную запилить. Тогда в идрисе я не осилил, а в haskell более-менее норм https://www.tweag.io/posts/2018-03-08-linear-sort.html

Много времени ушло?

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

соотвественно, мне не нужно было их переизобретать

в идрисе я примерно на переизобретении завис

другое дело, что в идрисе можно сделать OrdL доказанным, а тут нельзя и нужно полагаться на то, что он правильный

На радость @bravit111 предлагают ввести административную ответственность за кибербуллинг: https://twitter.com/batyshkaLenin/status/971928947389845505

@qnikst Крутая у вас команда. Она распределённая?

в основном да

есть офис в париже, где достаточно человек, и удаленщики

но те кто во франции не всегда в офисе

Круто. А у sparkle есть коммерческие клиенты (если не секрет)?

есть

собственно это оно под клиентов и было сделано

Здорово!

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

О, это интересно, надо будет разобраться с этим

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

а какие произведение и сумма используются?

можно уточнить вопрос, не уверен что я правильно его понял

в общем, все стрелки что есть в конструкторе данных считаются линейными

ну т.е. data Data = C1 x y | C2 z | C3 на уровне линейной типизации будет эквивалентно (x ⊗ y) ⊕ z ⊕ 1 ?

судя по утверждению насчёт сортировки списков - похоже, что так

да, так

@odomontois если нужно делать не линейные варианты то это можно через GADT синтакс, и тогда свои суммы и произведения можно сделать

как найти в какой lts входит пакет определнной версии?

@odomontois если нужно делать не линейные варианты то это можно через GADT синтакс, и тогда свои суммы и произведения можно сделать

скорее мне интересны линейные распаковочные варианты с &, ⅋ и T, но я догадываюсь, что их нужно выражать через а-ля чёрч-континюэйшн

если я правильно понимаю - то да

(про lts нашёл ответ)

http://www.well-typed.com/blog/2018/03/oop-in-haskell/ астрологи объявили неделю блогов от известных контор

После стольких лет до меня таки дошло что fix останавливаеться также как и foldr

После стольких лет до меня таки дошло что fix останавливаеться также как и foldr

Это вывод из статьи?

> The intention is to be sufficiently expressive to handle most if not all of the "undecidable" instances used by the mtl, lens and other libraries today in a manner that assures users of termination, and so doesn't induce the terror many users fear at the sight of UndecidableInstances.

Это вывод из статьи?

Это до меня дошло в начале

Это до меня дошло в начале

А что значит останавливается так же, как foldr?

Меня всегда fix пугал

Меня всегда fix пугал

😳 Чем?

Ну значит что функция не форсит аргумент

😳 Чем?

Шайтан

Так, а чем Fix отличается от Mu?

Всем привет, кто-нибудь может объяснить, пожалуйста, как это так?? f :: a -> b g :: c -> b :t g . f a -> c

:i (.)

Всем привет, кто-нибудь может объяснить, пожалуйста, как это так?? f :: a -> b g :: c -> b :t g . f a -> c

А что тебя смущает?

у g тип неправильный же

b -> c должен быть

(.) :: (b -> c) -> (a -> b) -> a -> c видимо я чего-то совсем не понимаю

а вот нет у g с -> b

Всем привет, кто-нибудь может объяснить, пожалуйста, как это так?? f :: a -> b g :: c -> b :t g . f a -> c

это самописанное или из ghci?

Так, это вообще какая-то разность функций получается

это ghci

Определения f и g - в студию

или :i (.) не оттуда же, или ошибка при копировании

писал профунктор: newtype PreYoneda f a x y = PreYoneda ((a -> x) -> f y) instance Functor f => Profunctor (PreYoneda f a) where -- dx -> ye -> ((a -> x) -> f y) -> ((a -> d) -> f e) dimap :: (d -> x) -> (y -> e) -> PreYoneda f a x y -> PreYoneda f a d e dimap dx ye (PreYoneda ax_fy) = PreYoneda $ \ax -> fmap ye (ax_fy (dx . ax))

все сжалось:( ща

https://i.imgur.com/xOOYBzs.png

Prelude> :t f f :: a -> b Prelude> :t g g :: c -> b Prelude> :t g . f g . f :: a -> c `

вон все как просили

https://i.imgur.com/PBIN8PQ.png

я думал-думал как реадизовать инстанс, но не придумал и списал, и никак не могу понять dx . ax :: a -> d

(dx :: d -> x) (ax :: -> a -> d) => dx . ax :: (a -> x)

при чем и почему здесь a -> d?

Prelude> :t f f :: a -> b Prelude> :t g g :: c -> b Prelude> :t g . f g . f :: a -> c `

а что тут ты показываешь? У тебя на входе (c->b) и (a -> b), тогда как у (.) на входе (b->c) и (a ->b)

а что тут ты показываешь? У тебя на входе (c->b) и (a -> b), тогда как у (.) на входе (b->c) и (a ->b)

я показываю те же типы которые попросил @basov_ae

при чем и почему здесь a -> d?

Наверно так будет лучше для полноты картины: https://i.imgur.com/n5Cj3L8.png

я показываю те же типы которые попросил @basov_ae

да они не сходятсяж

да они не сходятсяж

ghci так не посчитало

точней по-моему там ghc унифицирует разные типопеременные

Prelude> let g = undefined :: c -> b Prelude> let (.) = undefined :: (c -> b) -> (a -> b) -> c Prelude> let (.) = undefined :: (c -> b) -> (a -> b) -> (a -> c)

@basov_ae того, что было написано достаточно для моего комментария? разве в нём что-то было не так?

(dx :: d -> x) (ax :: -> a -> d) => dx . ax :: (a -> x)

этого ^

т.е. ты точку ввёл неканоническую чтоль?

да

(dx :: d -> x) (ax :: -> a -> d) => dx . ax :: (a -> x)

там разве не так происходит? (dx:: d ->x) (ax :: a -> x) => dx . ax :: (a -> d)

нет, конечно

астои

стоп.. секунуду

стандартная точка c унифицирует с b: λ> :t \(g :: c -> b) (f :: a -> b) -> g . f \(g :: c -> b) (f :: a -> b) -> g . f :: (c -> c) -> (a -> c) -> a -> c

PreYoneda f a d e ~ ((a -> d) -> f e) ax_fy :: ((a -> x) -> f y) ax :: a -> d dx :: d -> x dx . ax :: a -> x

это передается в ax_fy как и надо : as_fy (dx.ax) :: f y

ye :: y -> e, fmap ye (as_fy (dx.ax) :: f e

вроде все как надо

что-то я видимо сам себя запутал, спасибо