export Endo newtype wrapper

[mstksg]

Not sure if this is a desirable thing, but just a PR exporting the internal Endo wrapper. I was using one myself for some of my own code and thought it might be useful to not duplicate code, but I do understand that the Endo wraper does break some of the consistency in the singletons API, so it would also make sense to hide it as an internal tool only.

[RyanGlScott]

Hm. While I can understand the motivation for wanting this variation of Endo, I'm quite nervous about actually exporting it here for the sole reason that it's a different Endo than the one in Data.Monoid. One consequence of this is that we'll have two clashing Endos, so anyone who imports Data.Singletons.Prelude.Monoid will have to ensure that they don't use the wrong Endo in their code.

That's not to say that we haven't already done something like this before in singletons, since we redefined the ErrorMessage data type in Data.Singletons.TypeError module to make it more amenable to promotion. But that's a somewhat exceptional case since Data.Singletons.TypeError is rather sequestered off from the rest of singletons, so you must explicitly opt-in to it.

I think I would be somewhat more comfortable with this if the Endo stuff were exported from a different module (Data.Singletons.Prelude.Monoid.Endo, perhaps). There, we could redefine the Endo data type like so to allow it to be used at the value level as well:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Singletons.Prelude.Monoid.Endo (
  -- * @singletons@' version of 'Endo'
  Endo'(..), Endo, PEndo,

  -- * The 'Endo' singleton
  Sing(SEndo, sAppEndo),
  SEndo, AppEndo,

  -- * Defunctionalization symbols
  EndoSym0, EndoSym1,
  AppEndoSym0, AppEndoSym1
  ) where

import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.TH

newtype Endo' (p :: Type ~> Type ~> Type) a = Endo { appEndo :: p @@ a @@ a }
type Endo  = Endo' (TyCon2 (->))
type PEndo = Endo' (~>@#@$)

data instance Sing :: forall a. PEndo a -> Type where
  SEndo :: forall a (x :: a ~> a).
           { sAppEndo :: Sing x } -> Sing ('Endo x :: PEndo a)
type SEndo = (Sing :: PEndo a -> Type)
instance SingKind a => SingKind (PEndo a) where
  type Demote (PEndo a) = Endo (Demote a)
  fromSing (SEndo x) = Endo (fromSing x)
  toSing (Endo x) = withSomeSing x $ SomeSing . SEndo
instance SingI x => SingI ('Endo x:: PEndo a) where
  sing = SEndo sing
data EndoSym0 :: forall a. (a ~> a) ~> PEndo a
type instance Apply EndoSym0 x = 'Endo x
type EndoSym1 x = 'Endo x
instance SingI EndoSym0 where
  sing = singFun1 SEndo
instance SingI (TyCon1 'Endo :: (a ~> a) ~> PEndo a) where
  sing = singFun1 SEndo

$(singletons [d|
  type family AppEndo (x :: PEndo a) :: a ~> a where
    AppEndo ('Endo x) = x
  |])

$(singletonsOnly [d|
  instance Semigroup (PEndo a) where
          Endo x <> Endo y = Endo (x . y)
  instance Monoid (PEndo a) where
          mempty = Endo id
  |])

This way, those who are brave enough to use singletons' reinvention of Endo can import this module themselves, but other users won't be affected. What do you think?

[RyanGlScott]

Thoughts on #368 (comment), @mstksg?

[mstksg]

I've been working with some data types following a similar pattern. For the most part it seems to work well, but it does run counter to a lot of expectations when using promoted vs. promoted data types. For example, you could write code like:

$(singletonsOnly [d|
  blah :: [PEndo a] -> a -> a
  blah = appEndo . mconcat
  |])

blah :: [Endo a] -> a -> a
blah = appEndo . mconcat

But you can't "merge" the two layers together. So the link between the two is already a little superficial.

It makes sense for PEndo then to be different than normal Endo, so that users could use them both in the same module and to make it explicitly clear that the two are different types.

In this light, however, what would be the benefit of exporting the value-level type Endo = Endo' (TyCon2 (->)), instead of only defining the unparameterized data PEndo a = PEndo (a -> a) and having the user just use Data.Monoid.Endo for the value-level Endo? Does the library allow us to take advantage of the parameterization and link the two?

[RyanGlScott]

In this light, however, what would be the benefit of exporting the value-level type Endo = Endo' (TyCon2 (->)), instead of only defining the unparameterized data PEndo a = PEndo (a -> a) and having the user just use Data.Monoid.Endo for the value-level Endo?

Perhaps there isn't any advantage to doing this. I only suggested it since I was holding onto hope that this code might be made able to work simultaneously at the value- and type-level, but as you've just demonstrated, that idea falls apart pretty quickly, even in simple scenarios.

Does the library allow us to take advantage of the parameterization and link the two?

Only in the sense that we can use the same data type in the SingKind instance. But it turns out that we could just as well use the Endo from Data.Monoid, as this code snippet demonstrates:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Singletons.Prelude.Monoid.Endo (
  -- * 'Endo' (from "Data.Monoid")
  Endo(..),

  -- * Promoted 'Endo'
  PEndo(..),

  -- * The 'PEndo' singleton
  Sing(SPEndo, sAppPEndo),
  SPEndo, AppPEndo,

  -- * Defunctionalization symbols
  PEndoSym0, PEndoSym1,
  AppPEndoSym0, AppPEndoSym1
  ) where

import Data.Kind
import Data.Monoid (Endo(..))
import Data.Singletons.Prelude
import Data.Singletons.TH

newtype PEndo a = PEndo { appPEndo :: a ~> a }

data instance Sing :: forall a. PEndo a -> Type where
  SPEndo :: { sAppPEndo :: Sing x } -> Sing ('PEndo x)
type SPEndo = (Sing :: PEndo a -> Type)
instance SingKind a => SingKind (PEndo a) where
  type Demote (PEndo a) = Endo (Demote a)
  fromSing (SPEndo x) = Endo (fromSing x)
  toSing (Endo x) = withSomeSing x $ SomeSing . SPEndo
instance SingI x => SingI ('PEndo x) where
  sing = SPEndo sing

$(genDefunSymbols [''PEndo])
instance SingI PEndoSym0 where
  sing = singFun1 SPEndo
instance SingI (TyCon1 'PEndo) where
  sing = singFun1 SPEndo

$(singletons [d|
  type family AppPEndo (x :: PEndo a) :: a ~> a where
    AppPEndo ('PEndo x) = x
  |])

$(singletonsOnly [d|
  instance Semigroup (PEndo a) where
          PEndo x <> PEndo y = PEndo (x . y)
  instance Monoid (PEndo a) where
          mempty = PEndo id
  |])

It looks a bit strange, but it seems to work alright. And if you're happy with the ergonomics of that design, I'd be fine with including it in singletons.

[mstksg]

Right, I'll play around with just naming it PEndo for a bit.

I wonder though if there is a way to reduce the duplication in the definition of blah. Perhaps if there was some Promote typeclass (opposite of Demote), the two could be linked?

[RyanGlScott]

Perhaps if there was some Promote typeclass (opposite of Demote), the two could be linked?

FWIW, there exists a formulation of the SingKind machinery that does have a Promote type class. See the comments in this issue starting here, as well as an implementation of this idea here.

[RyanGlScott]

What is the status of this, @mstksg?

[mstksg]

I think I ended up being comfortable with just defining it in situations where I need it. Because I mostly used it internally, it was easier to overlook some of the trickier parts in the design. Because of this, it might be better off to not have this as a part of the core singletons library instead of some alternative "lifted utility" library.

[RyanGlScott]

Sounds reasonable. In that case, I'll go ahead and close this.