atzeus/reflectionwithoutremorse

Code accompanying the paper Reflection without Remorse:Revealing a hidden sequence to speed up monadic reflection

reflectionwithoutremorse's Issues

Make Data.LowerTSequence more efficient

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

LogicT isn't lazy enough

I would expect that

(pure 1 <|> pure 2) <|> undefined :: Logic

would be able to produce 1 and 2 before failing, but in fact it can only produce 1. The problem is the rather aggressive Empty matching in the definition of >< for bootstrapped queues. The fix is to remove that. The price of the fix is that if a bunch of emptys in a row get <|>ed onto the logic computation then views in multiple futures may each have to drop them. This is very similar, I think, to the cost of >=>ing a bunch of pures onto a free Kleisli category. Unfortunate, but unavoidable.

Lifted sequence coercions

Currently, you use data Any a where Any :: a b c -> Any a. This has a potential efficiency problem because of the extra constructor. I'm also not sure if it's entirely safe. As best I can tell, the officially sanctioned way to do this sort of thing is with the somewhat magical GHC.Prim.Any :: *, which is designed as a "safe" intermediary for unsafeCoerce. To use it, you'd just make a Seq Any or similar, and unsafeCoerce both on the way in and on the way out. GHC seems to promise not to play games with this type.

newtype FakeSequence a b c = FakeSequence (Seq Any)

Make type-aligned sequences polykinded

There's no sense in requiring the type indices to be of kind *. Adding {-# LANGUAGE PolyKinds #-} to appropriate places will fix this. I can try to open a pull request later.

MonadPlus instance for Logic has a bug

I noticed that runIdentity (observeAllT (mzero `mplus` pure 1)) was producing []. I then noticed this happened anytime mzero was the left argument to mplus.

The MonadPlus instance currently looks like this:

instance Monad m => MonadPlus (ML m) where
  mzero = ML empty
  mplus (toView -> m) n = fromView $ m >>= return . \case
       Nothing    -> Nothing
       Just (h,t) -> Just (h, cat t n) 
    where cat (ML l) (ML r) = ML $ l .>< r 

However, that first case means that mzero stops the rest of the computation. I changed the code to this:

instance Monad m => MonadPlus (ML m) where
  mzero = ML empty
  mplus (toView -> m) n = fromView $ m >>= \case
      Nothing -> toView n
      Just (h,t) -> return (Just (h, cat t n))
    where cat (ML l) (ML r) = ML $ l .>< r

And that seems to fix the issue. In particular, I have some local test code that compares breadth-first search and iterative deepening depth-first search and they now return equivalent results. And I was also able to confirm it now returns the same results as LogicT from Control.Monad.Logic. So I think the change I made is correct.

Encode shape invariant in CTQueue

Okasaki bootstraps with possibly-empty queues solely to reduce syntactic clutter, as he indicates in the first part of the relevant section. Since this is a library and not a book, that doesn't seem necessary here.

{-# LANGUAGE GADTs, PolyKinds, ExistentialQuantification,
    GeneralizedNewtypeDeriving, StandaloneDeriving, FlexibleContexts #-}

module Data.CTQueue where


import Data.Interface.TSequence
import Data.Monoid (Monoid (..))
import Control.Category
import Data.Semigroupoid
import Prelude hiding (id, (.))

-- Authors : Atze van der Ploeg and David Feuer
-- A purely functional catenable queue representation with
-- that turns takes a purely functional queue and turns in it into
-- a catenable queue, i.e. with the same complexity for (><) as for (|>)
-- Based on Purely functional data structures by Chris Okasaki 
-- section 7.2: Catenable lists

newtype CTQueue q c x y = CTQueue (AddEmpty (CTQueue1 q) c x y)
deriving instance TSequence q => TSequence (CTQueue q)

data AddEmpty q c x y where
  Empty :: AddEmpty q c x x
  Full :: q c x y -> AddEmpty q c x y

instance Semigroupoid (q c) => Category (AddEmpty q c) where
  id = Empty
  Empty . y = y
  x . Empty = x
  Full x . Full y = Full (x `o` y)

instance TQueue1 q => TSequence (AddEmpty q) where
  tempty = Empty
  tsingleton = Full . tsingleton1
  Empty |> y = Full (tsingleton1 y)
  Full xs |> y = Full (tpushr1 xs y)
  x <| Empty = Full (tsingleton1 x)
  x <| Full ys = Full (tsingleton1 x `append` ys)
  tviewl Empty = TEmptyL
  tviewl (Full xs) =
    case tviewl1 xs of
      y :|| ys -> y :| ys
  (><) = (>>>)

data CTQueue1 q c x y where
  CT :: c x y -> !(q (CTQueue1 q c) y z) -> CTQueue1 q c x z

instance TSequence q => Semigroupoid (CTQueue1 q c) where
  o = flip append

data TViewL1 q c x z = forall y . (:||) (c x y) (AddEmpty q c y z)

class TQueue1 q where
  tsingleton1 :: c x y -> q c x y
  tpushr1 :: q c x y -> c y z -> q c x z
  tviewl1 :: q c x y -> TViewL1 q c x y
  append :: q c x y -> q c y z -> q c x z

instance TSequence q => TQueue1 (CTQueue1 q) where
  tsingleton1 x = CT x tempty

  tpushr1 (CT y ys) x = CT y (ys |> CT x tempty)

  tviewl1 (CT x xs) = x :||
    case tviewl xs of
      TEmptyL -> Empty
      y :| ys -> Full (linkAll y ys)

  append (CT x xs) ys = CT x (xs |> ys)

linkAll :: TSequence q => CTQueue1 q c x y -> q (CTQueue1 q c) y z -> CTQueue1 q c x z
linkAll (CT pooh bah) q =
  case tviewl q of
      TEmptyL -> CT pooh bah
      s :| t -> CT pooh (bah |> linkAll s t)

CTQueue is too strict

Currently, you have

data CTQueue q c x y where
  C0 :: CTQueue q c x x
  CN :: c x y -> !(q (CTQueue q c) y z) -> CTQueue q c x z

According to Okasaki page 96, this only gives the correct amortized bounds when the queue is used ephemerally. He fixes it by making it lazier:

data CTQueue q c x y where
  C0 :: CTQueue q c x x
  CN :: c x y -> q (CTQueue q c) y z -> CTQueue q c x z

Further, I think we can safely make another change. In particular, Okasaki's implementation allows the CTQueue to be empty, which seems a bit strange when you go deeper into the tree. That is, there's never any reason to have CN x q where q has a C0 element. This suggests to me that it would be better to base the implementation on

data CTQueue1 q c x y where
  CT :: c x y -> q (CTQueue1 q c) y z -> CTQueue1 q c x z

and then handle the empty case separately. The extension to the empty case is pretty much trivial. The implementation of CTQueue1 looks like this (see the next comment instead).

data CTQueue1 q c x y where
  CT :: c x y -> q (CTQueue1 q c) y z -> CTQueue1 q c x z

data TViewL1 q c x y where
  TOneL :: c x y -> TViewL1 q c x y
  (:||) :: c x y -> q c y z -> TViewL1 q c x z

class TQueue1 q where
  tsingleton1 :: c x y -> q c x y
  tpushr1 :: q c x y -> c y z -> q c x z
  tviewl1 :: q c x y -> TViewL1 q c x y

instance TSequence q => TQueue1 (CTQueue1 q) where
  tsingleton1 x = CT x tempty
  tpushr1 (CT y ys) x = CT y (ys |> CT x tempty)
  tviewl1 (CT x xs) =
    case tviewl xs of
      TEmptyL -> TOneL x
      y :| ys -> x :|| linkAll y ys

linkAll :: TSequence q => CTQueue1 q c x y -> q (CTQueue1 q c) y z -> CTQueue1 q c x z
linkAll (CT pooh bah) q = CT pooh $
  case tviewl q of
      TEmptyL -> bah
      s :| t -> bah |> linkAll s t

append :: TSequence q => CTQueue1 q c x y -> CTQueue1 q c y z -> CTQueue1 q c x z
append (CT x xs) ys = CT x (xs |> ys)

cons :: TSequence q => c x y -> CTQueue1 q c y z -> CTQueue1 q c x z
cons x ys = CT x (tsingleton ys)

instance TSequence q => Semigroupoid (CTQueue1 q c) where
  o = flip append

Of course, some analysis would be required to ensure algorithmic performance, and testing to ensure actual performance.