ekmett / kan-extensions Goto Github PK
View Code? Open in Web Editor NEWKan extensions, Kan lifts, the Yoneda lemma, and (co)monads generated by a functor
License: Other
Kan extensions, Kan lifts, the Yoneda lemma, and (co)monads generated by a functor
License: Other
Day
gives a symmetric closed category over functors, and the internal hom objects are relatively easy to express in Haskell. Here's a sketch in my PureScript repo, but I could send a PR if you're interested in adding these?
https://pursuit.purescript.org/packages/purescript-day/3.0.0/docs/Data.Functor.Day#t:Hom
lens
uses Curried (Yoneda f) (Yoneda f)
and an internal liftCurriedYoneda
to implement confusing
. There are other applications where these pieces are more useful separately. For example, you can use a class
class GTraversable t where
gtraverse :: (a -> f b) -> t a -> Curried (Yoneda f) (Yoneda f) a
to implement generic deriving of Traversable
that seems to work almost exactly the same as GHC deriving (if you use a modified form of Generic1
). Perhaps it would even make sense to add a CurriedYoneda
type and explain what it can do for you.
Per #53 (comment), we should adopt GHC 8.4 as the minimum supported version of GHC. This will allow us to avoid some ugly CPP in various places (see #53 and #65 (comment) for examples).
There exist at least 2 conflicting candidatures:
-- Codensity (Const r) ~ Cont r
instance MonadCont (Codensity (Const r)) where
callCC f = Codensity (\k -> mapConst $ runCodensity (f (\x -> Codensity (\_ -> mapConst $ k x))) k)
where
mapConst :: Const r a -> Const r b
mapConst = Const . runConst
-- using callCC of m
instance MonadCont m => MonadCont (Codensity m) where
callCC f = join . lift $ callCC (\k -> return $ f (lift . k . return))
I am trying to use only Codensity
in a project. Unfortunately, kan-extensions
introduced many other dependencies. I wonder if we can split Codensity
into a small library and let kan-extensions
depend on it.
These instances exist already as Codensity
and Density
but they could be included for right/left Kan extensions of functors along themselves.
instance f₁ ~ f₂ => Applicative (Ran f₁ f₂) where
pure x = Ran (\k -> k x)
Ran f <*> Ran g = Ran (\bfr -> f (\ab -> g (bfr . ab)))
instance f₁ ~ f₂ => Monad (Ran f₁ f₂) where
return = pure
m >>= k = Ran (\c -> runRan m (\a -> runRan (k a) c))
-- etc.
and
instance f₁ ~ f₂ => Comonad (Lan f₁ f₂) where
duplicate (Lan f ws) = Lan (Lan f) ws
extract (Lan f a) = f a
-- etc.
Annoyingly the same can be done for Yoneda
/ Coyoneda
instance (Identity ~ id, Applicative f) => Applicative (Ran id f) where
pure a = Ran (\f -> pure (runIdentity (f a)))
-- ...
instance Identity ~ id => Foldable (Codensity id) where
foldMap f = foldMap f . lowerYoneda . ranToYoneda . codensityToRan
which overlaps and looks icky, is this a horrible idea?
There are some trivial instances for Managed
that could be implemented for Codensity
, the Monoid
instance is put to good use by Gabriel Gonzales in his Applied category theory and abstract algebra talk
instance Semigroup a => Semigroup (Codensity m a) where
(<>) = liftA2 (<>)
instance Monoid a => Monoid (Codensity m a) where
mempty = pure mempty
#if !(MIN_VERSION_base(5,0,0))
mappend = liftA2 (<>)
#endif
Same with Num
, Fractional
, Floating
.
Yoneda m >>= k = Yoneda (\f -> m id >>= \a -> runYoneda (k a) f)
I believe an alternative would be
Yoneda m >>= k = Yoneda (\f -> join . m $ \a -> runYoneda (k a) f)
The most obvious reason to prefer the current implementation is that it can take advantage of fmap id = id
optimizations in some situations. Is this the only reason?
improve :: Functor f => (forall m. MonadFree f m => m a) -> Free f a
improve m = lowerCodensity m
lowerCodensity :: Monad f => Codensity f a -> f a
The basic idea of improve
is that the passed action does not depend on the choice of free monad construction (I don't actually remember why this matters, but that's the idea). The specific choice of Free f
as the result monad, however, seems to be arbitrary. Thus
improve' :: (Functor f, MonadFree f m') =>
(forall m . MonadFree f m => m a) -> m' a
improve' m = lowerCodensity m
I doubt this will get accepted, but it's worth noting that Codensity
(and similar data types) can be made levity polymorphic
newtype Codensity (m::TYPE rep -> Type) a = Codensity
{ runCodensity :: forall b. (a -> m b) -> m b
}
If it's worth adding I'll make PR, if I understand correctly it can even be given a kind?
Codensity :: (TYPE rep -> TYPE rep') -> (TYPE rep'' -> Type)
src/Data/Functor/Kan/Ran.hs:108:18: error:
• Couldn't match type: forall (b1 :: k). (g b -> g b1) -> h b1
with: (a0 -> a0) -> h b
Expected: Ran g h (g b) -> (a0 -> a0) -> h b
Actual: Ran g h (g b) -> forall (b1 :: k). (g b -> g b1) -> h b1
I'll make a sweep on kan-extensions versions soon to see which other versions are affected and make according revisions, so this issue is for heads up purposes.
i need somehow to hoist underlying monad on CoT, is it possible?
data Lan :: (k -> Type) -> (k -> Type) -> (Type -> Type) where
Lan :: (g b -> a) -> (h b) -> Lan g h a
newtype Ran :: (k -> Type) -> (k -> Type) -> (Type -> Type) where
Ran :: { runRan :: forall b. (a -> g b) -> h b } -> Ran g h a
Configuring kan-extensions-4.1...
Dependency adjunctions ==4.2: using adjunctions-4.2
Dependency array ==0.4.0.1: using array-0.4.0.1
Dependency base ==4.6.0.1: using base-4.6.0.1
Dependency comonad ==4.2.2: using comonad-4.2.2
Dependency containers ==0.5.0.0: using containers-0.5.0.0
Dependency contravariant ==1.2: using contravariant-1.2
Dependency distributive ==0.4.4: using distributive-0.4.4
Dependency free ==4.9: using free-4.9
Dependency mtl ==2.1.3.1: using mtl-2.1.3.1
Dependency pointed ==4.1: using pointed-4.1
Dependency semigroupoids ==4.2: using semigroupoids-4.2
Dependency transformers ==0.3.0.0: using transformers-0.3.0.0
Using Cabal-1.20.0.0 compiled by ghc-7.6
Using compiler: ghc-7.6.3
Using install prefix: /var/lib/jenkins/.cabal
Binaries installed in:
/var/lib/jenkins/workspace/Stackage/ghcversion/7.6.3/stackage/sandbox/bin
Libraries installed in:
/var/lib/jenkins/workspace/Stackage/ghcversion/7.6.3/stackage/sandbox/lib/x86_64-linux-ghc-7.6.3/kan-extensions-4.1
Private binaries installed in: /var/lib/jenkins/.cabal/libexec
Data files installed in:
/var/lib/jenkins/workspace/Stackage/ghcversion/7.6.3/stackage/sandbox/share/x86_64-linux-ghc-7.6.3/kan-extensions-4.1
Documentation installed in:
/var/lib/jenkins/workspace/Stackage/ghcversion/7.6.3/stackage/sandbox/share/doc/kan-extensions-4.1
Configuration files installed in: /var/lib/jenkins/.cabal/etc
Using alex version 3.1.3 found on system at:
/var/lib/jenkins/workspace/Stackage/ghcversion/7.6.3/stackage/sandbox/bin/alex
Using ar found on system at: /usr/bin/ar
No c2hs found
Using cpphs version 1.18.5 found on system at:
/var/lib/jenkins/workspace/Stackage/ghcversion/7.6.3/stackage/sandbox/bin/cpphs
No ffihugs found
Using gcc version 4.8 found on system at: /usr/bin/gcc
Using ghc version 7.6.3 found on system at: /opt/ghc/7.6.3/bin/ghc
Using ghc-pkg version 7.6.3 found on system at: /opt/ghc/7.6.3/bin/ghc-pkg
No greencard found
Using haddock version 2.13.2 found on system at: /opt/ghc/7.6.3/bin/haddock
Using happy version 1.19.4 found on system at:
/var/lib/jenkins/workspace/Stackage/ghcversion/7.6.3/stackage/sandbox/bin/happy
Using haskell-suite found on system at: haskell-suite-dummy-location
Using haskell-suite-pkg found on system at: haskell-suite-pkg-dummy-location
No hmake found
Using hpc version 0.6 found on system at: /opt/ghc/7.6.3/bin/hpc
Using hsc2hs version 0.67 found on system at: /opt/ghc/7.6.3/bin/hsc2hs
Using hscolour version 1.20 found on system at:
/var/lib/jenkins/workspace/Stackage/ghcversion/7.6.3/stackage/sandbox/bin/HsColour
No hugs found
No jhc found
Using ld found on system at: /usr/bin/ld
No lhc found
No lhc-pkg found
No nhc98 found
Using pkg-config version 0.26 found on system at: /usr/bin/pkg-config
Using strip found on system at: /usr/bin/strip
Using tar found on system at: /bin/tar
No uhc found
Component build order: library
creating dist/build
creating dist/build/autogen
Building kan-extensions-4.1...
Preprocessing library kan-extensions-4.1...
Building library...
creating dist/build
/opt/ghc/7.6.3/bin/ghc --make -fbuilding-cabal-package -O -outputdir dist/build -odir dist/build -hidir dist/build -stubdir dist/build -i -idist/build -isrc -idist/build/autogen -Idist/build/autogen -Idist/build -optP-include -optPdist/build/autogen/cabal_macros.h -package-name kan-extensions-4.1 -hide-all-packages -no-user-package-db -package-db /var/lib/jenkins/workspace/Stackage/ghcversion/7.6.3/stackage/sandbox/package-db -package-db dist/package.conf.inplace -package-id adjunctions-4.2-ab681c076c70761a0b3dee65d9a42ab8 -package-id array-0.4.0.1-3b78425c10ff2dad7acf7e8c8ae014c3 -package-id base-4.6.0.1-8aa5d403c45ea59dcd2c39f123e27d57 -package-id comonad-4.2.2-59217784e907b1aabcf64b8f191b3815 -package-id containers-0.5.0.0-ab1dae9a94cd3cc84e7b2805636ebfa2 -package-id contravariant-1.2-4f56a055aa93b13d2ce191f3d54d247d -package-id distributive-0.4.4-f35281d827800032c5fe74c053ad0474 -package-id free-4.9-1f9be52b839623900055875a2e6cc133 -package-id mtl-2.1.3.1-4779b0d7ec31de052f42201cd7318025 -package-id pointed-4.1-7efcc70f43b003dbd2a0f8d5aa3c1c17 -package-id semigroupoids-4.2-c5ebe1bff925106f246dfa0e69df0b94 -package-id transformers-0.3.0.0-ff2bb6ac67241ebb987351a3db564af0 -XHaskell98 Control.Comonad.Density Control.Monad.Co Control.Monad.Codensity Data.Functor.Contravariant.Day Data.Functor.Contravariant.Yoneda Data.Functor.Contravariant.Coyoneda Data.Functor.Day Data.Functor.Kan.Lan Data.Functor.Kan.Lift Data.Functor.Kan.Ran Data.Functor.Kan.Rift Data.Functor.Yoneda Data.Functor.Coyoneda -Wall
src/Data/Functor/Contravariant/Day.hs:44:8:
Could not find module `Data.Proxy'
It is a member of the hidden package `tagged-0.7.2'.
Perhaps you need to add `tagged' to the build-depends in your .cabal file.
Use -v to see a list of the files searched for.
In particular:
foldr c n (Coyoneda k a) = foldr (c . k) n a
foldl f b (Coyoneda k a) = foldl (\acc -> f acc . k) go b a
-- foldl', foldr', foldl1, foldr1 similarly
toList (Coyoneda k a) = map k (toList a) -- but this is arguably worse than the default!
length (Coyoneda _ a) = length a
null (Coyoneda _ a) = null a
Unfortunately, I don't believe it's possible to do anything about fold
, maximum
, minimum
, sum
, product
, or elem
.
The library mmtl has a MonadFix (Codensity m)
instance
-- still need to prove that MonadFix laws hold
instance MonadFix m => MonadFix (Codensity m) where
mfix :: (a -> Codensity m a) -> Codensity m a
mfix f = lift (mfix (lowerCodensity . f))
https://hackage.haskell.org/package/mmtl-0.1/docs/Control-Monad-Codensity.html
Useful?
composeRan' :: forall compose f g a. Composition compose => Ran f (Codensity g) a -> Ran (compose f g) g a
composeRan' = coerce (composeRan @compose @f @g @g @a)
decomposeRan' :: forall compose f g a. (Composition compose, Functor f) => Ran (compose f g) g a -> Ran f (Codensity g) a
decomposeRan' = coerce (decomposeRan @compose @f @g @g @a)
https://ghc.haskell.org/~hvr/buildreports/kan-extensions.html
src/Data/Functor/Kan/Rift.hs:108:10:
Illegal equational constraint g ~ h
(Use -XTypeFamilies to permit this)
In the context: (Functor g, g ~ h)
While checking the context of an instance declaration
In the instance declaration for `Applicative (Rift g h)'
Currently,
lowerCodensity :: Monad m => Codensity m a -> m a
lowerCodensity a = runCodensity a return
We could AMP that up to
lowerCodensity :: Applicative f => Codensity f a -> f a
lowerCodensity a = runCodensity a pure
Whether that's useful or not is another question, but it's possible.
I stumbled across these while implementing Termination Combinators Forever. The termination combinator type Test
described therein is the contravariant Coyoneda transformation of the Equivalence
functor. Its combinators are characterized by these instances: given Test a ~ Coyoneda Equivalence a
, then chosen
and divided
are exactly the combinators eitherT
and pairT
, and conquer
is alwaysT
. These can then be derived automatically, all thanks to -XDerivingVia
. (Equivalence
technically demands symmetry which WQOs violate, but for deriving instances we can ignore it since we don't derive any others that need it.)
instance Divisible f => Divisible (Coyoneda f) where
conquer :: Coyoneda f a
conquer = Coyoneda id conquer
{-# INLINE conquer #-}
divide :: (a -> (b, c)) -> Coyoneda f b -> Coyoneda f c -> Coyoneda f a
divide cleave (Coyoneda fb b) (Coyoneda fc c)
= Coyoneda (bimap fb fc . cleave) (divided b c)
{-# INLINE divide #-}
instance Decidable f => Decidable (Coyoneda f) where
lose :: (a -> Void) -> Coyoneda f a
lose f = Coyoneda id (lose f)
{-# INLINE lose #-}
choose :: (a -> Either b c) -> Coyoneda f b -> Coyoneda f c -> Coyoneda f a
choose fork (Coyoneda fb b) (Coyoneda fc c)
= Coyoneda (bimap fb fc . fork) (chosen b c)
{-# INLINE choose #-}
Proof of equality is left as a simple exercise:
-- Generalized implementation of 'Test' from "Termination Combinators Forever"
newtype Test (a :: Type) = Test (Coyoneda Equivalence a)
-- DerivingVia is amazing.
deriving Contravariant via (Coyoneda Equivalence)
deriving Divisible via (Coyoneda Equivalence)
deriving Decidable via (Coyoneda Equivalence)
-- 'WQO' constructor, backwards-compatible with the
-- termination-combinators package/paper.
pattern WQO :: forall a. forall b. (a -> b) -> (b -> b -> Bool) -> Test a
pattern WQO co eq = Test (Coyoneda co (Equivalence eq))
{-# COMPLETE WQO #-}
Also, while playing around more, I stumbled upon the following instance for contravariant Day
:
contract :: Divisible f => Day f f a -> f a
contract (Day ca cb k) = divide k ca cb
instance Divisible f => Divisible (Day f f) where
conquer :: Day f f a
conquer = diag conquer
divide :: (a -> (b, c)) -> Day f f b -> Day f f c -> Day f f a
divide cleave fb fc = Day (contract fb) (contract fc) cleave
I feel there is something lurking within Divisible (Day f f)
that can get us to Divisible (Coyoneda f)
, but I'm not sure.
Some of these may belong in Data.Functor.Kan.Lan
.
From Monads Need Not Be Endofunctors
fold :: (forall xx. (f xx -> a) -> (g x -> lan)) -> (Lan f g a -> lan)
fold a (Lan b c) = a b c
-- as in paper, or
fold' :: Lan f g a -> (forall lan. (forall xx. (f xx -> a) -> (g xx -> lan)) -> lan)
fold' (Lan a b) c = c a b
hoistLan :: (g ~> g') -> (Lan f g ~> Lan f g')
hoistLan tau = fold (\g -> Lan g . tau)
The tensor that is defined F ·_J G = Lan J F · G
data Comp :: (k -> Type) -> (k -> Type) -> (k' -> Type) -> (k' -> Type) where
Comp :: (j xx -> g a) -> (f xx -> Comp j f g a)
foldComp :: (forall xx. (j xx -> g a) -> (f xx -> r)) -> (Comp j f g a -> r)
foldComp f (Comp a b) = f a b
intro2 :: m ~> Comp rel m rel
intro2 = Comp id
elim1 :: Comp rel rel m ~> m
elim1 = foldComp id
disassoc :: Comp rel (Comp rel f g) h ~> Comp rel f (Comp rel g h)
disassoc = foldComp $ \g -> foldComp $ \f -> Comp (Comp g . f)
is really more useful with some kind of relative monad
class RelMonad m rel where
royalReturn :: rel ~> m
relativeBind :: (rel a -> m b) -> (m a -> m b)
unit :: RelMonad m rel => rel ~> m
unit = royalReturn
mult :: RelMonad m rel => Comp rel m m ~> m
mult = foldComp relativeBind
I spotted this on ncatlab
Proposition 4.1. For F:C→D a 𝒱-enriched functor between small 𝒱-enriched categories we have
- the left Kan extension along F takes representable presheaves C(c,−):C→𝒱 to their image under F:
Lan FC(c,−)≃D(F(c),−)
for all c ∈ C.
An in Haskell this translates (roughly) to a Representable
instance for Lan
:
instance (Functor f, Representable g) => Distributive (Lan f g) where
distribute :: Functor h => h (Lan f g a) -> Lan f g (h a)
distribute = distributeRep
instance (Functor f, Representable g) => Representable (Lan f g) where
type Rep (Lan f g) = f (Rep g)
index :: Lan f g a -> (f (Rep g) -> a)
index (Lan f g) = f . fmap (index g)
tabulate :: (f (Rep g) -> a) -> Lan f g a
tabulate = (`Lan` tabulate id)
I noticed it was missing from the library.
And change (Functor f, Eq (f a)) => Eq (Coyoneda f a)
to
Eq1 f => Eq1 (Coyoneda f)
?
Would that need a major bump (following up the free
4 -> 5)?
I was reading Oleg's Extensible Effects: An Alternative to Monad Transformers.
The coroutine for arbitrary effects Eff r
is the same as Codensity (Free r)
.
data VE w r = Val w | E (r (VE w r))
newtype Eff r a = Eff{runEff :: ∀ w. (a → VE w r) → VE w r}
So I wondered if the send
function had some usefulness in the library, admin
is already a specialization of lowerCodensity
send :: (∀ w. (a → VE w r) → r (VE w r)) → Eff r a
send f = Eff $ \k → E (f k)
admin :: Eff r w → VE w r
admin (Eff m) = m Val
but send
, producing a Codensity (Free f) a
, is not in the library:
send :: (forall x. (a -> Free f x) -> f (Free f x)) -> Codensity (Free f) a
send eff = Codensity \next -> Free (eff next)
There is the following instance:
instance ComonadCofree f w => MonadFree (Co f) (Co w)
Essentially, we could require only ComonadCofree g w
for some g
for which there is a pairing with f
. But since we don't have a type class for that, and since inference would be presumably pretty horrible, I think it makes sense to just choose Co f
for g
.
What do you think?
Found this construction, and I thought I should make an issue here for reference (and possible future inclusion).
Through some isomorphism arithmetic, it's possible to find a direct-style Co
:
forall r. w (a -> r) -> r
~ forall r x. (x -> a -> r) -> w x -> r
~ forall r x. ((x, a) -> r) -> w x -> r
~ forall x. w x -> (x, a)
which is easily generalizable to a monad transformer:
newtype CovT w m a = CovT { runCovT :: forall x. w x -> m (x, a) }
instance Functor m => Functor (CovT w m) where
fmap f cov = CovT $ \w -> (fmap . fmap) f (runCovT cov w)
instance (Comonad w, Monad m) => Applicative (CovT w m) where
pure a = CovT $ \w -> pure (extract w, a)
(<*>) = ap
instance (Comonad w, Monad m) => Monad (CovT w m) where
m >>= f = CovT $ \w -> do
(w', a) <- runCovT m (duplicate w)
runCovT (f a) w'
The obvious difference here is that CovT w m
is covariant in m
. Also, unlike CoT
, CovT (Store s) m
is directly isomorphic to StateT s m
(rather than the CPS version of StateT
). In the same way, CovT ((,) r) m ~ ReaderT r m
, CovT ((->) s) m ~ WriterT s m
, etc.
The IOSim s
Monad has the same instances as Codensity (SimA s)
except with oneShot
. Could be added to the Codensity
instances, giving the compiler better hints and allowing the io-sim library to derive via Codensity
.
newtype IOSim s a = IOSim { unIOSim :: forall r. (a -> SimA s r) -> SimA s r }
instance Functor (IOSim s) where
{-# INLINE fmap #-}
fmap f = \d -> IOSim $ oneShot $ \k -> unIOSim d (k . f)
instance Applicative (IOSim s) where
{-# INLINE pure #-}
{-# INLINE (<*>) #-}
{-# INLINE (*>) #-}
pure = \x -> IOSim $ oneShot $ \k -> k x
(<*>) = \df dx -> IOSim $ oneShot $ \k -> unIOSim df (\f -> unIOSim dx (\x -> k (f x)))
(*>) = \dm dn -> IOSim $ oneShot $ \k -> unIOSim dm (\_ -> unIOSim dn k)
instance Monad (IOSim s) where
{-# INLINE (>>=) #-}
{-# INLINE (>>) #-}
return = pure
(>>=) = \dm f -> IOSim $ oneShot $ \k -> unIOSim dm (\m -> unIOSim (f m) k)
(>>) = (*>)
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.7.20130625
$ cabal install kan-extensions
Resolving dependencies...
Configuring kan-extensions-3.6...
Building kan-extensions-3.6...
Preprocessing library kan-extensions-3.6...
[ 1 of 10] Compiling Data.Functor.Yoneda.Reduction ( src/Data/Functor/Yoneda/Reduction.hs, dist/build/Data/Functor/Yoneda/Reduction.o )
[ 2 of 10] Compiling Data.Functor.Yoneda ( src/Data/Functor/Yoneda.hs, dist/build/Data/Functor/Yoneda.o )
src/Data/Functor/Yoneda.hs:81:11: Warning:
Rule "lower/lift=id" may never fire because ‛.’ might inline first
Probable fix: add an INLINE[n] or NOINLINE[n] pragma on ‛.’
src/Data/Functor/Yoneda.hs:82:11: Warning:
Rule "lift/lower=id" may never fire because ‛.’ might inline first
Probable fix: add an INLINE[n] or NOINLINE[n] pragma on ‛.’
[ 3 of 10] Compiling Data.Functor.Kan.Rift ( src/Data/Functor/Kan/Rift.hs, dist/build/Data/Functor/Kan/Rift.o )
[ 4 of 10] Compiling Data.Functor.Kan.Lift ( src/Data/Functor/Kan/Lift.hs, dist/build/Data/Functor/Kan/Lift.o )
src/Data/Functor/Kan/Lift.hs:51:27:
Cannot instantiate unification variable ‛a0’
with a type involving foralls: forall x. h x -> g (z x)
Perhaps you want -XImpredicativeTypes
In the first argument of ‛Lift’, namely ‛(fmap f . g)’
In the expression: Lift (fmap f . g)
In an equation for ‛fmap’: fmap f (Lift g) = Lift (fmap f . g)
src/Data/Functor/Kan/Lift.hs:51:36:
Cannot instantiate unification variable ‛a0’
with a type involving foralls: forall x. h x -> g (z x)
Perhaps you want -XImpredicativeTypes
In the second argument of ‛(.)’, namely ‛g’
In the first argument of ‛Lift’, namely ‛(fmap f . g)’
src/Data/Functor/Kan/Lift.hs:67:10:
Cannot instantiate unification variable ‛b0’
with a type involving foralls: forall a. f a -> g (z a)
Perhaps you want -XImpredicativeTypes
In the expression: flip runLift
In an equation for ‛toLift’: toLift = flip runLift
src/Data/Functor/Kan/Lift.hs:67:15:
Cannot instantiate unification variable ‛b0’
with a type involving foralls: forall x. f x -> g (z x)
Perhaps you want -XImpredicativeTypes
In the first argument of ‛flip’, namely ‛runLift’
In the expression: flip runLift
Failed to install kan-extensions-3.6
cabal: Error: some packages failed to install:
kan-extensions-3.6 failed during the building phase. The exception was:
ExitFailure 1
Adding {-# LANGUAGE ImpredicativeTypes #-} to Lift.hs makes it build successfully, but I am leery of this extension, having been bitten by it in the past.
It's possible to encode Day
differently:
data Day2__ :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
Day2__ :: f xx -> g (xx -> a) -> (Day2__ f g) a
data Day3__ :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
Day3__ :: f (xx -> a) -> g xx -> (Day3__ f g) a
Users might want access to them for some reason, we can expose pattern synonyms to access them
day2 :: forall f g a. Functor g => Day f g a -> Day2__ f g a
day2 (Day fa gb f) = Day2__ fa (flip f gb)
day3 :: Functor f => Day f g a -> Day3__ f g a
day3 (Day fa gb f) = Day3__ (fmap f fa) gb
pattern Day2 :: forall f g a. Functor g => forall xx. f xx -> g (xx -> a) -> Day f g a
pattern Day2 fa gb <- (day2 -> Day2__ fa gb)
where Day2 fa gb = Day fa gb (&)
pattern Day3 :: forall f g a. Functor f => forall xx. f (xx -> a) -> g xx -> Day f g a
pattern Day3 fa gb <- (day3 -> Day3__ fa gb)
where Day3 fa gb = Day fa gb id
Useful or not? I didn't put thought into choosing encodings or names.
Is there a particular reason that Codensity
does not implement MonadReader
? If not, I'd be happy to submit a patch. Thanks!
Make Codensity
kind polymorphic
Codensity :: (k -> Type) -> (Type -> Type)
Prelude: I don't know if it's worth trying to do this, or if the more precise arity analysis is better than theoretical allocation improvements.
We can legally define
instance MonadTrans Codensity where
lift = frob
frob :: forall m a . Monad m => m a -> Codensity m a
frob = coerce (blah (Mag (>>=)) :: m a -> Mag2 m a)
newtype Mag m a = Mag (forall b . m a -> (a -> m b) -> m b)
newtype Mag2 m a = Mag2 (forall b . (a -> m b) -> m b)
blah :: Mag m a -> m a -> Mag2 m a
blah (Mag p) q = Mag2 (p q)
blah
is obviously the identity (up to arity), because all it does is remove a newtype constructor and put a different one on. The effect is to shift the forall b
to the right of an arrow; this does not change the run-time representation because type lambdas compile away. Unfortunately, I don't see a way to convince GHC that blah
is just a cast. I believe, however, that it should be safe to define blah = unsafeCoerce id
.
src/Data/Functor/Yoneda.hs:166:3:
Type indexes must match class instance head
Found Yoneda f' but expected
Yoneda g'
In the type synonym instance declaration for Rep' In the instance declaration for
Representable (Yoneda g)'
Failed to install kan-extensions-4.0
cabal: Error: some packages failed to install:
kan-extensions-4.0 failed during the building phase. The exception was:
ExitFailure 1
There is some talk on reddit if the functor arguments of Ran
, Lan
should be swapped, for example defining ibind
and iextend
for them
ibind :: (a -> Ran k j b) -> (Ran j i a -> Ran k i b)
ibind k (Ran m) = Ran (\c -> m (\a -> runRan (k a) c))
iextend :: (Lan k j a -> b) -> (Lan k i a -> Lan j i b)
iextend f (Lan h ws) = Lan (f . Lan h) ws
yields a swapped argument order from the type class
class IxApplicative m => IxMonad m where
ibind :: (a -> m j k b) -> (m i j a -> m i k b)
class IxCopointed w => IxComonad w where
iextend :: (w j k a -> b) -> (w i k a -> w i j b)
Thoughts?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.