Add proofs of Monad laws for SplineT (WIP)

[mitchellwrosen]

Still todo: associativity (fixes #11)

[schell]

@mitchellwrosen feel free to push more changes when you have them! I'm working on documentation for 1.0 so I figured I'd merge this now.

[mitchellwrosen]

@schell Will do, I got a bit stuck =P

[schell]

@mitchellwrosen - what if we wrote the proofs in Idris? Do you have any experience in Idris? I just got Type Driven Development and I think it may be a good project.

[mitchellwrosen]

Yeah! I read TDD about eight months ago and it's fantastic! I think you'll have to rejigger the types to be non-recursive before you can prove any laws about them.

Sounds like a fun project indeed... please dump any in-progress work into this issue or a branch and I'll be happy to follow along. I can't say I'll be much help, I haven't ever tried proving laws (only simple properties as in the book).

[schell]

Hmmm - yeah the totality checks don't pass without littering assert_total around. I asked the guys in #idris on freenode and they said that's acceptable. Do you see another way? I don't think it's possible to ditch recursion, as the whole strategy is based on mealy machines. Maybe a pure version would do the trick? I'm not totally certain how useful the effect full version is, though it's nice for code organization, like pipes, conduits or machines. I'll experiment.

Here's what I have so far:

record VaryingT (m : Type -> Type) (input : Type) (output : Type)  where
  constructor VT
  runVT : input -> m (output, Inf $ VaryingT m input output)

constant : Applicative m => b -> Inf $ VaryingT m a b
constant b = assert_total $ VT $ \ _ => pure (b, constant b)

Monad m => Functor (VaryingT m a) where
  map f v = assert_total $ VT $ \ x => do
    (b, v2) <- runVT v x
    pure (f b, map f v2)

Monad m => Applicative (VaryingT m a) where
  pure b = constant b
  vf <*> vx = assert_total $ VT $ \ a => do
    (f, vf1) <- runVT vf a
    (x, vx1) <- runVT vx a
    pure (f x, vf1 <*> vx1)

Monad m => Category (VaryingT m) where
  id = assert_total $ VT $ \ a => pure (a, id)
  vf . vg = assert_total $ VT $ \ a => do
    (b, vg2) <- runVT vg a
    (c, vf2) <- runVT vf b
    pure (c, vf2 . vg2)

Monad m => Arrow (VaryingT m) where
  arrow f = assert_total $ VT $ \ a => pure (f a, arrow f)
  first v = assert_total $ VT $ \ (a, c) => do
    (b, v2) <- runVT v a
    pure ((b, c), first v2)

(Monad m, Num b) => Num (VaryingT m a b) where
  (+) = liftA2 (+)
  (*) = liftA2 (*)
  fromInteger = pure . fromInteger

(Monad m, Fractional b) => Fractional (VaryingT m a b) where
  (/) = liftA2 (/)
  recip = map recip

varM : Monad m => (a -> m b) -> VaryingT m a b
varM f = VT $ \ a => do
  b <- f a
  pure (b, varM f)

[schell]

Looks like totality checks pass for a pure variant.

record Varying (input : Type) (output : Type)  where
  constructor V
  runV : input -> (output, Inf $ Varying input output)

Functor (Varying a) where
  map f v = V $ \ x => let (b, v2) = runV v x in (f b, map f v2)

constV : b -> Varying a b
constV b = V $ \ _ => (b, constV b)

Applicative (Varying a) where
  pure = constV
  vf <*> vx = V $ \ a => let (f, vf1) = runV vf a
                             (x, vx1) = runV vx a
                         in (f x, vf1 <*> vx1)

[mitchellwrosen]

I think I do have a solution for this - using the coyoneda lemma to massage out the partiality. I can't exactly explain why Idris thinks one version is not total, yet the other is, but it's the trick that John Wiegley used in his pipes proofs (see https://github.com/jwiegley/coq-pipes/blob/master/src/Pipes/Internal.v#L95)

Anywho, the coyoneda lemma says that these are isomorphic (f is a functor):

f a ~ ∃b. (b -> a, f b)

Here are the isomorphisms:

data Co : (Type -> Type) -> Type -> Type where
  MkCo : (b -> a) -> f b -> Co f a

toCo : f a -> Co f a
toCo x = MkCo id x

fromCo : Functor f => Co f a -> f a
fromCo (MkCo f x) = map f x

runVT would then look like this:

record VaryingT (m : Type -> Type) (a : Type) (b : Type)  where
  constructor VT
  runVT : a -> (x -> (b, Inf (VaryingT m a b)), m x)

[mitchellwrosen]

Whoops, that runVT might be wrong; I'm not sure how to make an existential type variable...

Idris says runVT has this type:

runVT : (rec : VaryingT m input output) ->
        input ->
        (free_x rec -> (output, Inf (VaryingT m input output)),
         m (free_x rec))

What's free_x?

[mitchellwrosen]

Whew, I made some progress... first, I switched to data type syntax so that the type variables are existentially quantified (I'm sure this is possible with records but I don't know the syntax):

data VaryingT (Type -> Type) -> Type -> Type -> Type where
  VT : (a -> (x -> (b, Inf (VaryingT m a b)), m x)) -> VaryingT m a b

Now the type of runVT is actually a dependent pair, since 'x' is existentially quantified. In other words, this type is wrong:

runVT : VaryingT m a b -> a -> (x -> (b, Inf (VaryingT m a b)), m x)

because the caller doesn't and can't know what x is inside the original VaryingT m a b.

I struggled with this for a bit, but what we actually have is just a dependent pair where the value upon which the right side of the pair depends is Type!

runVT : VaryingT m a b -> a -> DPair Type (\x => (x -> (b, Inf (VaryingT m a b)), m x))
runVT x (VT f) = { for you to do =) }

Whoa O_O

[schell]

This is all blowing my mind a little. I'm going to have to read up on coyoneda lemma. What is the m x? My guess is all will be revealed once I understand coyoneda lemma.

[mitchellwrosen]

Oh, the m x is "half" of the original m (b, VaryingT m a b) (which Idris can't see as total).

So, I simply turned this:

m (b, VaryingT m a b)

into this:

∃x.
  (m x)
  and
  (x -> (b, VaryingT m a b))

per the isomorphism

f a ~ ∃b. (b -> a) and (f b)

where f is a functor.