{-# LANGUAGE RankNTypes , TypeOperators , MultiParamTypeClasses , TypeInType , TypeFamilies , UndecidableInstances , StandaloneDeriving #-} import Prelude hiding (Functor, map) import Data.Kind import Data.Function (fix) class Category cat where cat_id :: a `cat` a cat_compose :: b `cat` c -> a `cat` b -> a `cat` c instance Category (->) where cat_id = id cat_compose = (.) instance Category (~>) where cat_id = Nat id cat_compose f g = Nat (runNat f . runNat g) class (Category cat1, Category cat2) => Functor cat1 cat2 (f :: obj1 -> obj2) where type C f (a :: obj1) :: Constraint map :: C f a => (a `cat1` b) -> (f a `cat2` f b) instance Functor (->) (->) Maybe where type C Maybe a = () map = fmap instance Functor (~>) (->) Fix where type C Fix f = (Functor (->) (->) f, C f (Fix f)) map eta = fix (\f -> Fix . runNat eta . map f . unFix) newtype f ~> g = Nat { runNat :: forall x. f x -> g x } newtype Fix f = Fix { unFix :: f (Fix f) } deriving instance Show (f (Fix f)) => Show (Fix f) toList :: Maybe a -> [a] toList (Just x) = [x] toList Nothing = [] x :: Fix Maybe x = Fix (Just (Fix (Just (Fix Nothing)))) y :: Fix [] y = map (Nat toList) x

хитрый constraint в Fix

потому что ты сам Кметт?

чего это?

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

видел я выше запостил через fundeps вариант?

хитрый constraint в Fix

да, вот в нем и неудобство, слишком много старнный констрейтов придется требовать для обобщенного кода, который будет такое использовать

видел я выше запостил через fundeps вариант?

да, но вроде он не поменяет ничего

и там такое как выше не опишешь уже)

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

мне кажется, в этом что-то не так. в инстансах дополнительные ограничения должны быть слева от головы

чего это?

(просто попытка пошутить)

а по поводу категориальности, есть еще такой пакет https://github.com/sjoerdvisscher/data-category

мне кажется, в этом что-то не так. в инстансах дополнительные ограничения должны быть слева от головы

делают ассоциативны ограничения внутри, когда нечего ограничивать в голове

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

есть ещё https://github.com/mikeizbicki/subhask

по-хорошему надо как-то так: class Category (cat :: k -> k -> *) where type Obj cat (a :: k) :: Constraint id :: Obj cat a => cat a a (.) :: (Obj cat a, Obj cat b, Obj cat c) => cat b c -> cat a b -> cat a c instance Category (->) where type Obj (->) a = () id = P.id (.) = (P..) newtype f ~> g = Nat { runNat :: forall x. f x -> g x } instance Category (~>) where type Obj (~>) a = () id = Nat id (.) f g = Nat (runNat f . runNat g) class (Category cat1, Category cat2, forall a. Obj cat1 a => Obj cat2 (f a)) => Functor (cat1 :: k1 -> k1 -> *) (cat2 :: k2 -> k2 -> *) (f :: k1 -> k2) where map :: (Obj cat1 a, Obj cat1 b) => (a `cat1` b) -> (f a `cat2` f b)

но GHC у меня слишком старый для QuantifiedContexts

это тебе и даст C Fix f => C f (Fix f)

можно для Nat попросить type Obj (~>) f = Functor f

хм, ну да, это все таки ограниченная категория объектов, а не ограничения на функтор

я пытался ставить ограничения на конструтор ~>, но они конечно не вытягивались в функторе

{-# LANGUAGE RankNTypes , TypeOperators , MultiParamTypeClasses , TypeInType , TypeFamilies , UndecidableInstances , StandaloneDeriving , FlexibleContexts , ConstraintKinds #-} import Prelude hiding (Functor, map) import Data.Kind import Data.Function (fix) class Category (cat :: k -> k -> Type) where type Object cat (a :: k) :: Constraint cat_id :: Object cat a => a `cat` a cat_compose :: (Object cat a, Object cat b, Object cat c) => b `cat` c -> a `cat` b -> a `cat` c instance Category (->) where type Object (->) a = () cat_id = id cat_compose = (.) instance Category (~>) where type Object (~>) f = Functor (->) (->) f cat_id = Nat id cat_compose f g = Nat (runNat f . runNat g) class (Category cat1, Category cat2) => Functor cat1 cat2 (f :: obj1 -> obj2) where map :: (Object cat1 a, Object cat1 b, Object cat2 (f a), Object cat2 (f b)) => (a `cat1` b) -> (f a `cat2` f b) instance Functor (->) (->) Maybe where map = fmap instance Functor (->) (->) [] where map = fmap instance Functor (~>) (->) Fix where map eta = fix (\f -> Fix . runNat eta . map f . unFix) newtype (f :: Type -> Type) ~> (g :: Type -> Type) = Nat { runNat :: forall x. f x -> g x } newtype Fix f = Fix { unFix :: f (Fix f) } deriving instance Show (f (Fix f)) => Show (Fix f) type HaskFunctor = Functor (->) (->) hoist :: (HaskFunctor f, HaskFunctor g) => (forall x. f x -> g x) -> Fix f -> Fix g hoist f = map (Nat f) toList :: Maybe a -> [a] toList (Just x) = [x] toList Nothing = [] x :: Fix Maybe x = Fix (Just (Fix (Just (Fix Nothing)))) y, z :: Fix [] y = hoist toList x z = map (Nat toList) x

намного лучше

{-# LANGUAGE RankNTypes , TypeOperators , MultiParamTypeClasses , TypeInType , TypeFamilies , UndecidableInstances , StandaloneDeriving , FlexibleContexts , ConstraintKinds #-} import Prelude hiding (Functor, map) import Data.Kind import Data.Function (fix) class Category (cat :: k -> k -> Type) where type Object cat (a :: k) :: Constraint cat_id :: Object cat a => a `cat` a cat_compose :: (Object cat a, Object cat b, Object cat c) => b `cat` c -> a `cat` b -> a `cat` c instance Category (->) where type Object (->) a = () cat_id = id cat_compose = (.) instance Category (~>) where type Object (~>) f = Functor (->) (->) f cat_id = Nat id cat_compose f g = Nat (runNat f . runNat g) class (Category cat1, Category cat2) => Functor cat1 cat2 (f :: obj1 -> obj2) where map :: (Object cat1 a, Object cat1 b, Object cat2 (f a), Object cat2 (f b)) => (a `cat1` b) -> (f a `cat2` f b) instance Functor (->) (->) Maybe where map = fmap instance Functor (->) (->) [] where map = fmap instance Functor (~>) (->) Fix where map eta = fix (\f -> Fix . runNat eta . map f . unFix) newtype (f :: Type -> Type) ~> (g :: Type -> Type) = Nat { runNat :: forall x. f x -> g x } newtype Fix f = Fix { unFix :: f (Fix f) } deriving instance Show (f (Fix f)) => Show (Fix f) type HaskFunctor = Functor (->) (->) hoist :: (HaskFunctor f, HaskFunctor g) => (forall x. f x -> g x) -> Fix f -> Fix g hoist f = map (Nat f) toList :: Maybe a -> [a] toList (Just x) = [x] toList Nothing = [] x :: Fix Maybe x = Fix (Just (Fix (Just (Fix Nothing)))) y, z :: Fix [] y = hoist toList x z = map (Nat toList) x

такс, чем это отличается от предидущего?

нет констрейтов в Functor

они вынесены в более правильное место - в категорию (~>) - категория конкретно эндофункторов в Hask, а не всех типоконструкторов, из-за этого больше не нужны констрейты в функторе

я ща экспериментирую с data Dict (c :: Constraint) where Dict :: c => Dict c class (Category cat1, Category cat2) => Functor (cat1 :: k1 -> k1 -> *) (cat2 :: k2 -> k2 -> *) (f :: k1 -> k2) where obj :: forall a. Obj cat1 a => Dict (Obj cat2 (f a)) map :: (Obj cat1 a, Obj cat1 b) => (a `cat1` b) -> (f a `cat2` f b)

они вынесены в более правильное место - в категорию (~>) - категория конкретно эндофункторов в Hask, а не всех типоконструкторов, из-за этого больше не нужны констрейты в функторе

тоесть для обычной стрелки констрейнт юнит?

тоесть для обычной стрелки констрейнт юнит?

да, это категория всех типов

я ща экспериментирую с data Dict (c :: Constraint) where Dict :: c => Dict c class (Category cat1, Category cat2) => Functor (cat1 :: k1 -> k1 -> *) (cat2 :: k2 -> k2 -> *) (f :: k1 -> k2) where obj :: forall a. Obj cat1 a => Dict (Obj cat2 (f a)) map :: (Obj cat1 a, Obj cat1 b) => (a `cat1` b) -> (f a `cat2` f b)

это же пакет который будет не нужен после QuantifiedConstraints

у меня GHC старый

хм, ну да, это все таки ограниченная категория объектов, а не ограничения на функтор

теоретически можно ещё попробовать написать категорию функторов

да, это категория всех типов

ну и соответственно для естественных преобразований, это категория всех функторов

и может быть категорию всех категорий используя Dict

теоретически можно ещё попробовать написать категорию функторов

ну так разве это не она

да, а можно "The category with categories as objects and functors as arrows." ?

class (Category cat1, Category cat2) => Functor (cat1 :: k1 -> k1 -> *) (cat2 :: k2 -> k2 -> *) (f :: k1 -> k2) where obj :: forall a. Obj cat1 a => Dict (Obj cat2 (f a)) map :: (Obj cat1 a, Obj cat1 b) => (a `cat1` b) -> (f a `cat2` f b) instance Functor (->) (->) Maybe where obj = Dict map = fmap instance Functor (->) (->) [] where obj = Dict map = fmap newtype Fix f = Fix { unFix :: f (Fix f) } deriving instance Show (f (Fix f)) => Show (Fix f) instance Functor (~>) (->) Fix where obj = Dict map eta = fix (\f -> Fix . runNat eta . map f . unFix)

@kana_sama ты смотрел Коналовское решение? https://github.com/conal/concat

нет ещё

class (Category cat1, Category cat2) => Functor (cat1 :: k1 -> k1 -> *) (cat2 :: k2 -> k2 -> *) (f :: k1 -> k2) where obj :: forall a. Obj cat1 a => Dict (Obj cat2 (f a)) map :: (Obj cat1 a, Obj cat1 b) => (a `cat1` b) -> (f a `cat2` f b) instance Functor (->) (->) Maybe where obj = Dict map = fmap instance Functor (->) (->) [] where obj = Dict map = fmap newtype Fix f = Fix { unFix :: f (Fix f) } deriving instance Show (f (Fix f)) => Show (Fix f) instance Functor (~>) (->) Fix where obj = Dict map eta = fix (\f -> Fix . runNat eta . map f . unFix)

Dict как чит)

он ща пригодится, попробую категорию категорий написать

всё сложно, надо думать data CatT (cat1 :: k1 -> k1 -> *) (cat2 :: k2 -> k2 -> *) = forall (f :: k1 -> k2). Functor cat1 cat2 f => CatT (Proxy f)

https://twitter.com/dshevchenko_biz/status/1043459549389352960

Простите за оффтоп, друзья, но я знаю, что здесь много Вимеров...

@ulysses4ever ты про ICFP спрашивал? я вот приехал

@ulysses4ever ты про ICFP спрашивал? я вот приехал

Круто!А я только выезжаю :) Надо законтачиться будет

пиши, как приедешь

привет а никто не знает есть ли какая-нибудь простая в использовании библиотека для поддержки multiline strings с интерполяцией?

https://hackage.haskell.org/package/interpolate ?

спасибо!

привет а никто не знает есть ли какая-нибудь простая в использовании библиотека для поддержки multiline strings с интерполяцией?

Смотря, что подразумевается под интерполяцией. Если самая простая для мультистрочных строк, где можно вставлять текстовые переменные, то лучше neat-interpolation: * http://hackage.haskell.org/package/neat-interpolation У interpolate, как я вижу, в зависимостях haskell-src-meta, а это значит, что зависимости будут билдиться полчаса, а если на виртуалке с 2Гб памяти, так и вовсе может не сбилдиться. Я бы порекомендовал избегать библиотек с очень тяжёлыми зависимостями, если нет острой необходимости.

спасибо, NeatInterpolation - то что нужно

Подскажите какую-нибудь (хорошую) статью/пост про перформанс серванта, как делать и как не делать. Здесь выше у кого-то проект с ним не собирался из-за того, что в память не влезал.

Совет простой, не особо мудри с тайплевел фичами, я сам на грабли наступил тогда

По умолчанию сервант хорошо работает, памяти хватит

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

Ещё к выжиранию памяти может привести использование vinyl в body запросов

Не думаю, что в эти грабли можно попасть, не зная уже многих других не type level грабель

да и вывод инстансов аесона через дженерики

если рекорды большие

Меня через ghcjs вывод аесон инстансов на TH бесит, компилит модуль с 200 инстансами минут 10

но на дженериках наверное бы в рантайме боль была

да они вроде не тормозные

Помню на uniplate поверх Generic были большие лаги

А TH нормально справился

ERROR: S client not available

юниплейт-то тормозной

Вместе с Generic это было очень заметно

А можно cabal new-build воспретить пытаться что-то притащить по сети?

Можно. --offline

а у варпа есть возможность сказкать forkWarpProcess

чтобы в случае graceful shutdown этот процесс бы тоже ожидался?

https://alexknvl.com/posts/counting-type-inhabitants.html

https://alexknvl.com/posts/counting-type-inhabitants.html

We’ve encountered a problem proving that from . to = id Это следует из натуральности f Лемма Йонеды ставит в эквивалентность не весь ∀ x. (a -> x) -> f x, а его натуральный сабсет. Для натуральной f верно что для любой g f. fmap g == fmap g. f

есть просто такая ката https://www.codewars.com/kata/yoneda-lemma/haskell

и там как раз про инхабитантов тоже есть

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

We’ve encountered a problem proving that from . to = id Это следует из натуральности f Лемма Йонеды ставит в эквивалентность не весь ∀ x. (a -> x) -> f x, а его натуральный сабсет. Для натуральной f верно что для любой g f. fmap g == fmap g. f

ага, а натуральность следует из free theorems

ага, а натуральность следует из free theorems

Натуральность сама по себе ниоткуда не следует. ∀ x. (a -> x) -> f x строго больше, чем множество естественных

Для утверждения о множествах безотносительно хаскеля это тоже верно

следует из fmap id = id

и из free theorems

следует из fmap id = id

Нет, конечно. Это просто закон функтора

ок, давай по порядку

Давай

> Это следует из натуральности f

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

forall a. f a -> g a более широкое множество, чем множество естественных трансформаций из f в g

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

f - это имя полиморфной функции, которая используется в твоём доказательстве

это не полиморфная функция

это type constructor

ну т.е. f : Type -> Type, только если в этом смысле

естественные трансформации = natural transformation?

это не полиморфная функция

from . to $ f = from $ f id = \g -> fmap g (f id) вот из твоей ссылки

ааа

Это доказуемо, когда f - не любая полиморфная функция, а удовлетворяющая условию натуральности, которое я написал

We’ve encountered a problem proving that from . to = id Это следует из натуральности f Лемма Йонеды ставит в эквивалентность не весь ∀ x. (a -> x) -> f x, а его натуральный сабсет. Для натуральной f верно что для любой g f. fmap g == fmap g. f

f. fmap g == fmap g. f для любой g