Make Data.LowerTSequence more efficient

[treeowl]

Currently, you use

data AsUnitLoop a b c where 
   UL :: !a -> AsUnitLoop a () ()
newtype MSeq s a = MSeq { getMS :: s (AsUnitLoop a) () () }

The trouble is that this sprays UL constructors all through the type-aligned sequence.

Once #2 is fixed, there's another (somewhat disgusting) way that seems reasonably likely to be safe:

newtype AsUnitLoop a (b :: Void) (c :: Void) = UL a

data MSeq (s :: (Void -> Void -> *) -> Void -> Void -> *) a where
  MSeq :: { getMS :: !(s (AsUnitLoop a) i j) } -> MSeq s a

Here's the nasty bit:

voidEqual :: forall p q . (p :: Void) :~: (q :: Void)
voidEqual = unsafeCoerce (Refl :: p :~: p)

Now

instance TSequence s => Sequence (MSeq (s :: (Void -> Void -> *) -> Void -> Void -> *)) where
  empty      = MSeq tempty
  singleton  = MSeq . tsingleton . UL
  MSeq (l :: s (AsUnitLoop a) i j) .>< MSeq (r :: s (AsUnitLoop a) m n) =
    case voidEqual :: j :~: m of
      Refl -> MSeq $ l >< r
  MSeq l .|> x    = MSeq $ l |> UL x
  x .<| MSeq r    = MSeq $ UL x <| r
  viewl (MSeq s)   = case tviewl s of
     TEmptyL      -> EmptyL
     UL h :| t -> h :< MSeq t
  viewr  (MSeq s)   = case tviewr s of
     TEmptyR      -> EmptyR
     p :|< UL l -> MSeq p :> l

[treeowl]

I forgot to explain. It would be nice to be able to use the () kind, whose only "moral" inhabitant is '(). Unfortunately, () is also populated by stuck types and type loops, so I suspect it will be dangerous to assume that s c i j and s c m n can be composed; perhaps j ~ '() and m ~ Any. I'm not entirely sure how dangerous that is, but it scares me. The only inhabitants of Void are stuck types and type loops, which I think cannot be distinguished by any means, so I believe it should be safe to assume they're all the same.

[atzeus]

I agree that it works, but it's not pretty :)

If you want to create a pull request for it, I'll merge it.

Cheers

[treeowl]

I'm not quite ready to put the pull request together, but here's the latest draft in case my computer decides to bite the dust or something. I replaced my existential wrapper with a rank-2 one to completely erase the wrappers.

{-# LANGUAGE GADTs, FlexibleInstances,UndecidableInstances #-}
{-# LANGUAGE KindSignatures, DataKinds, PolyKinds, RankNTypes #-}
{-# LANGUAGE EmptyDataDecls, TypeOperators, ScopedTypeVariables #-}


module Data.LowerTSequence where

import Data.Interface.Sequence
import Data.Interface.TSequence
import Data.Foldable
import Data.Traversable
import Data.Typeable (Typeable)
import Data.Type.Equality
import Control.Applicative hiding (empty)
import Data.Monoid
import Unsafe.Coerce

-- A private copy of Data.Void.Void. Keeping this private
-- might reduce the potential for other people's dirty tricks
-- to interact badly with our dirty trick.
data Void

-- This postulate is kind of disgusting. It would be really nice to be
-- able to use the () kind, whose only proper inhabitant is '().
-- Unfortunately, it also has *improper* (stuck) inhabitants.
-- Void seems to be somewhat better in this regard, containing
-- only stuck types and type loops. Hopefully this can't be used
-- to break type safety, but I can't quite guarantee it.
voidEqual :: (p :: Void) :~: (q :: Void)
voidEqual = unsafeCoerce (Refl :: p :~: p)

newtype AsUnitLoop a (b :: Void) (c :: Void) = UL a

-- This looks a bit weird, doesn't it? We can't ever *instantiate*
-- the type indices to anything in particular, but that's okay,
-- because we never actually need to. It would be easier to just use
-- an existential
--
-- data MSeq (s :: ...) a where
--   MSeq :: forall i j . !(s (AsUnitLoop a) i j) -> MSeq s a
--
-- but that wraps each lowered sequence in a worthless constructor.
-- Using a universally quantified newtype instead, we completely
-- avoid memory overhead.
newtype MSeq (s :: (Void -> Void -> *) -> Void -> Void -> *) a =
        MSeq { getMS :: forall i . s (AsUnitLoop a) i i }

-- Generalize @s (AsUnitLoop a) i j@ to @MSeq s a@.
mseq :: forall s a (i :: Void) (j :: Void) . s (AsUnitLoop a) i j -> MSeq s a
mseq t = MSeq
  (gcastWith (voidEqual :: p :~: i) $ gcastWith (voidEqual :: p :~: j) t ::
    forall p . s (AsUnitLoop a) p p)

instance TSequence s => Sequence (MSeq (s :: (Void -> Void -> *) -> Void -> Void -> *)) where
  empty      = MSeq tempty
  singleton x = MSeq $ tsingleton $ UL $ x
  MSeq l .>< MSeq r = mseq (l >< r)
  MSeq l .|> x    = MSeq $ l |> UL x
  x .<| MSeq r    = MSeq $ UL x <| r
  viewl (MSeq s)   = case tviewl s of
     TEmptyL      -> EmptyL
     UL h :| t -> h :< mseq t
  viewr  (MSeq s)   = case tviewr s of
     TEmptyR      -> EmptyR
     p :|< UL l -> mseq p :> l

instance TSequence s => Monoid (MSeq s a) where
  mempty = empty
  mappend = (.><)

instance TSequence s => Functor (MSeq s) where
  fmap f = map where
   map q = case viewl q of
     EmptyL -> empty
     h :< t -> f h .<| map t 

instance TSequence s => Foldable (MSeq s) where
  foldMap f = fm where
   fm q = case viewl q of
     EmptyL -> mempty
     h :< t -> f h `mappend` fm t 

instance TSequence s => Traversable (MSeq s) where
  sequenceA q = case viewl q of
     EmptyL -> pure empty
     h :< t -> pure (.<|) <*> h <*> sequenceA t