FormationAI / dhall-bhat

Tasty meal of Dhall
66 stars 11 forks source link

Yo Yoneda #27

Closed FintanH closed 6 years ago

FintanH commented 6 years ago

Adds Yoneda to our arsenal so that we can inline Functor.maps better during normalisation.

Test examples:


    let Either = ./Either/Type

in  let Yoneda = ./Yoneda/Type

in  let emap = ./Either/Functor Text

in  let fmap = (./Yoneda/Functor (Either Text)).map

in  let plusOne = λ(i : Natural) → i + 1

in  let plusTwo = λ(i : Natural) → i + 2

in  let foo =
            λ(y : Yoneda (Either Text) Natural)
          → fmap Natural Natural plusOne (fmap Natural Natural plusTwo y)

in  let bar =
            λ(e : Either Text Natural)
          → ./Yoneda/lift (Either Text) emap Natural e

in    λ(e : Either Text Natural)
    → ./Yoneda/lower (Either Text) Natural (foo (bar e))

vs


    let Either = ./Either/Type

in  let emap = (./Either/Functor Text).map

in  let plusOne = λ(i : Natural) → i + 1

in  let plusTwo = λ(i : Natural) → i + 2

in    λ(e : Either Text Natural)
    → emap Natural Natural plusOne (emap Natural Natural plusTwo e)

There'll be 2 merge expressions in the second dhall expr compared to 1 in the first

FintanH commented 6 years ago

This looks mostly good. I would just remove the duplication from Yoneda/liftYoneda so that it’s Yoneda/lift, and the same for lower.

Good shout! Much cleaner