search

FormationAI / dhall-bhat

Tasty meal of Dhall
66 stars 11 forks source link

Redefine Codensity and Yoneda in terms of Ran #30

Closed joneshf closed 6 years ago

joneshf commented 6 years ago

Creating an issue for visibility, and so I don't forget to do this :sweat_smile:.

As discussed in slack, there's a formulation of Codensity and Yoneda in terms of Kan extensions. In particular, given the right Kan extension:

-- Ran
  λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ ∀(b : Type) → (a → f b) → g b

We can define Codensity:

-- Codensity
λ(m : Type → Type) → Ran m m

We can also define Yoneda:

Ran Id

Does that seem about right? More than happy to submit a PR for this.

joneshf commented 6 years ago

cc @FintanH, @sellout

FintanH commented 6 years ago

@joneshf Yup! That looks legit 😄

FintanH commented 6 years ago

When you're happy to submit a PR can you run make lint and make compile to ensure that everything is clean and compiles :) we'll eventually get CI to confirm that this is done, but unfortunately it isn't done yet.

joneshf commented 6 years ago

Want a (separate) PR for CI as well?

FintanH commented 6 years ago

We may be adding CI on our side. Need to ping our boy in Formation to check the status on that. Thanks for the offer 😄

FintanH commented 6 years ago

Closed via #31