{-# 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

они вынесены в более правильное место - в категорию (~>) - категория конкретно эндофункторов в 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)

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

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

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

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)

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

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

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

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

следует из fmap id = 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