search

VictorCMiraldo / generics-mrsop

MIT License
21 stars 1 forks source link

Use efficient indexed Sum from Oleg's Freer Monads paper #39

Closed arianvp closed 5 years ago

arianvp commented 6 years ago

It makes Pattern matching on Indexed Sums O(1) which will make our converisons a bit more efficient.

Also, it might fool the compiler into fixing #6 http://hackage.haskell.org/package/freer-effects-0.3.0.1/docs/Data-OpenUnion.html http://hackage.haskell.org/package/freer-effects-0.3.0.1/docs/Data-OpenUnion-Internal.html

serras commented 6 years ago

There is also the package freer-simple, which seems better maintained, in case you want to add a dependency on a package.

VictorCMiraldo commented 5 years ago

Branch victor-efficient-NS compiles just fine with

data NS :: (k -> *) -> [k] -> * where
  NS :: (IsNat n) => Constr' xs n -> p (Lkup n xs) -> NS p xs

newtype Constr' (xs :: [k]) (n :: Nat)
= Constr' { unConstr' :: Word }

But this does not fix the memory usage issue. :frowning_face:

arianvp commented 5 years ago

Given this a second thought today. Possible reason why it's still slow is because a lot of the code still uses Constr instead of Constr' and we're calling fromConstr and toConstr' in a lot of places. This wil mean we're still pattern matching on N-ary sums directly (just in some other ismorphic form that also requires the compiler to type-check exhaustiveness?)

Perhaps we should rewrite match and inj to use Constr' directly; instead of Constr

edit: Oh wait, but just compiling from and to is already slow... so that can't be it :/