Make Codensity kind and levity polymorphic

[treeowl]

With TypeInType, we can get

Codensity :: (k -> TYPE rep) -> Type -> Type

I don't know if the polymorphism in k is useful; it was readily available, so I took it. I actually have an application in mind for polymorphism in rep. The primitive package offers

indexArrayM :: Monad m => Array a -> Int -> m a

Now what if I want to recover the underlying functionality of indexArray# from that? One option would be to use the data Box a = Box a "lifted identity" monad. Another would be to use a custom-written Cont monad (a clone of the one from transformers). But I realized that Codensity almost works off the shelf, if we just add a bit of extra polymorphism. With this patch, I can write

iarr# :: Array a -> Int -> (# a #)
iarr# ar i = runCodensity (indexArrayM ar i) (\a -> (# a #))

and get exactly the Core I want

iarr# :: forall a. Array a -> Int -> (# a #)
[GblId,
 Arity=2,
 Caf=NoCafRefs,
 Str=<S(S),1*U(U)><S(S),1*U(U)>,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=False)
         Tmpl= \ (@ a_aetV)
                 (ar_aetE [Occ=Once!] :: Array a_aetV)
                 (i_aetF [Occ=Once!] :: Int) ->
                 case i_aetF of { GHC.Types.I# i#_aeun [Occ=Once] ->
                 case ar_aetE of { Array ds2_aeur [Occ=Once] ->
                 GHC.Prim.indexArray# @ a_aetV ds2_aeur i#_aeun
                 }
                 }}]
iarr#
  = \ (@ a_aetV) (ar_aetE :: Array a_aetV) (i_aetF :: Int) ->
      case i_aetF of { GHC.Types.I# i#_aeun ->
      case ar_aetE of { Array ds2_aeur ->
      GHC.Prim.indexArray# @ a_aetV ds2_aeur i#_aeun
      }
      }

[treeowl]

By the way: it is also quite possible to make ContT work with this sort of thing. Unfortunately, that means convincing Ross Paterson to do it.

[ekmett]

The levity polymorphism seems to work out to be free.

On the other hand, the PolyKinds can wind up with many potential instances becoming flexible

Consider the following fairly artificial example,

instance (Applicative f, Monoid m) => Monoid (Codensity f m)

It wasn't flexible before PolyKinds were added, but afterwards, (as shown by haddock)

instance (Applicative f, Monoid m) => Monoid (Codensity * f m)

is a flexible instance. So until something monomorphizes the kind of the argument, the instance isn't selectable, leading to more situations where instance selection gets stuck.

At present, IIRC, we already have PolyKinds turned on, so we've already paid this latter cost.

[treeowl]

Good point. Perhaps we should unflex the instances by fixing the kind in the constraint where appropriate?

[ekmett]

The reason I accepted the original proposal to adopt PolyKinds for this data type was that as I recall, none of the existing instances happened to run afoul of this issue, but its a thing I consider whenever I get an enthusiastic email asking me to PolyKind all the things.

[treeowl]

Maybe I got the version wrong...

On Mar 13, 2018 8:39 AM, "Ryan Scott" notifications@github.com wrote:

@RyanGlScott commented on this pull request.

I didn't notice this until it was merged—one minor comment.

In src/Control/Monad/Codensity.hs https://github.com/ekmett/kan-extensions/pull/52#discussion_r174112973:

import Data.Typeable

endif

+#if __GLASGOW_HASKELL__ >= 802 +import GHC.Exts (TYPE)

Levity polymorphism has been around since GHC 8.0—is there a reason you only enabled it on 8.2 or later?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/ekmett/kan-extensions/pull/52#pullrequestreview-103408988, or mute the thread https://github.com/notifications/unsubscribe-auth/ABzi_YkEb6rQiiZyzfh7TYYpC_GpsxDpks5td74LgaJpZM4SoGqw .

[treeowl]

@RyanGlScott, FYI, in a new PR, I tried 8.0 and the compiler panicked. TypeInType was pretty experimental then.

[RyanGlScott]

Ah! Thanks for confirming.

[Icelandjack]

@ekmett Is this at all better than the flexible version?

instance (f ~~ f', Applicative f', Monoid m) => Monoid (Codensity (f::k -> Type) m)

[treeowl]

I submitted a PR suggesting this approach. I think it works for everything except MonadTrans.

On Mar 16, 2018 3:39 PM, "Icelandjack" notifications@github.com wrote:

@ekmett https://github.com/ekmett Is this at all better than the flexible version?

instance (f ~~ f', Applicative f', Monoid m) => Monoid (Codensity (f::k -> Type) m)

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/ekmett/kan-extensions/pull/52#issuecomment-373823634, or mute the thread https://github.com/notifications/unsubscribe-auth/ABzi_f1hfjJx12VPtO94rPcj-R3IDqhyks5tfBUDgaJpZM4SoGqw .

[Icelandjack]

Great! #53