well-typed / falsify

Other
36 stars 5 forks source link

Think about generation of functions #11

Closed edsko closed 1 year ago

edsko commented 1 year ago

Some references:

Pretty sure that at least promote is not definable, because it relies on capturing the PRNG. Would it make sense to have an additional constructor in Gen for this...?

data Gen a where
  Pure  :: a -> Gen a
  Prim  :: Prim a -> Gen a
  Bind  :: Gen a -> (a -> Gen b) -> Gen b
  STree :: Gen SampleTree

perhaps...? How would that then shrink...?

edsko commented 1 year ago

Related suggestion from @phadej for a monad-law-preserving

data Freer f a where
  Pure :: a -> Freer f a
  Bind :: f b -> (b -> Freer f a) -> Freer f a

newtype Prim a = Prim (SMGen -> a)

interpret :: SMGen -> Freer Prim a -> a
interpret _ (Pure x)         = x
interpret g (Bind (Prim f) k = case split g of
  (g1, g2) -> interpret g2 (k (f g1))

Note that Prim can capture the SMGen here, which would enable us to define promote. If we can make something like this work, that would be nice, but it requires some thought.