Slightly tweak Rep and Fix for pedagogical reasons

[arianvp]

If we shuffle around the arguments of Rep, it is clear it returns a Functor over Set^n

data RepF :: (kon -> *) -> [[[Atom kon]]] -> (Nat -> *) -> (Nat -> *) where
  RepF :: Rep ki phi (Lkup ix codes) -> RepF ki codes phi ix

then we can use a heterogenous Fix that doesnt mention generics-mrsop constructs at all.
I'm not sure if we actually want it in code, but it's at least a nice comment to show there's
a direct relationship with the Fix that most people already know.

data Fix :: ((Nat -> *) -> (Nat -> *)) -> (Nat -> *) where
  Fix :: f (Fix f) n -> Fix f n


a  ~  Fix (RepF (Code a))

vs

data Fix :: (* -> *) -> * where
  Fix :: f (Fix f) -> Fix f

[serras]

The Fix using Nat is nothing else that the one from multirec, but using the more modern DataKinds extension.

[arianvp]

Correct

[VictorCMiraldo]

We have to count how many functions use the partially applied `Rep`. If I'm notistaken, there was a reason for the order of parameters. I'll look into it later today!

…

On Tue, Mar 5, 2019, 23:42 Arian van Putten ***@***.***> wrote: Correct — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#44 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AE-l31UlXB97Q0uOqk2w4BtZBtAF1xT9ks5vTuTYgaJpZM4bfLFc> .

[VictorCMiraldo]

@arianvp , I'm not sure I understand your proposal.

Currently, we have:

newtype Rep (ki :: kon -> *) (phi :: Nat -> *) (code :: [[Atom kon]])
  = Rep { unRep :: NS (PoA ki phi) code }

data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (phi :: Nat -> *) (n :: Nat) =
  AnnFix (phi n)
         (Rep ki (AnnFix ki codes phi) (Lkup n codes))

type Fix ki codes = AnnFix ki codes (Const ())

If I got it right, you are proposing we move to:

newtype Rep (ki :: kon -> *) (code :: [[Atom kon]]) (phi :: Nat -> *) 
  = Rep { unRep :: NS (PoA ki phi) code }

data AnnFix (ki :: kon -> *) (codes :: [[[Atom kon]]]) (ann :: Nat -> *) (n :: Nat) =
  AnnFix (ann n) (Rep ki (Lkup n codes) (AnnFix ki codes ann) )

type Fix ki codes = AnnFix ki codes (Const ())

Note I changed the parameter name to AnnFix from phi to ann. We should eventually do that.
Moreover, if we are messing with these datatypes, we will have to separate Fix and AnnFix.
I'm ok with that as long as Fix becomes a newtype after that. That is, It only makes sense
to decouple this dependency if we win something. I don't think pedagogical value counts here.
We have the papers that were written precisely for that.

[VictorCMiraldo]

Discussing with @arianvp we concluded:

• Drop AnnFix and Fix dependency
• The reordering of params won't happen. We can't do Lkup ix codes in Rep because we
  want to use Rep for opaque types aswell, ie, Rep :: Atom ki -> *.
• We won't depend on sop-core. Our combinators are different than theirs and simpler than theirs.
  Bringing it in for two types is not worth it.