FormationAI / dhall-bhat

Tasty meal of Dhall
66 stars 11 forks source link

Introduce the left Kan extension #41

Closed joneshf closed 5 years ago

joneshf commented 5 years ago

Counterpart of #31. Also introduces Coyoneda f a, and Density f a.

Similar optimizations as #27:

Coyoneda ```Dhall let Either = ./Either/Type in let Coyoneda = ./Coyoneda/Type in let emap = ./Either/functor Text in let fmap = (./Coyoneda/functor (Either Text)).map in let plusOne = λ(i : Natural) → i + 1 in let plusTwo = λ(i : Natural) → i + 2 in let foo = λ(y : Coyoneda (Either Text) Natural) → fmap Natural Natural plusOne (fmap Natural Natural plusTwo y) in let bar = ./Coyoneda/lift (Either Text) Natural in λ(e : Either Text Natural) → ./Coyoneda/lower (Either Text) emap Natural (foo (bar e)) ``` ```Dhall ∀(e : < Left : Text | Right : Natural >) → < Right : Natural | Left : Text > ``` ```Dhall λ(e : < Left : Text | Right : Natural >) → merge { Left = λ(x : Text) → < Left = x | Right : Natural > , Right = λ(y : Natural) → < Right = (y + 2) + 1 | Left : Text > } e ```
Density ```Dhall let NonEmptyList = ./NonEmptyList/Type in let Density = ./Density/Type in let applicative = ./NonEmptyList/applicative in let fmap = (./Density/functor NonEmptyList).map in let plusOne = λ(i : Natural) → i + 1 in let plusTwo = λ(i : Natural) → i + 2 in let foo = λ(y : Density NonEmptyList Natural) → fmap Natural Natural plusOne (fmap Natural Natural plusTwo y) in let bar = ./Density/lift NonEmptyList ./NonEmptyList/comonad Natural in λ(e : NonEmptyList Natural) → ./Density/lower NonEmptyList applicative Natural (foo (bar e)) ``` ```Dhall ∀(e : { head : Natural, tail : List Natural }) → { head : Natural, tail : List Natural } ``` ```Dhall λ(e : { head : Natural, tail : List Natural }) → { head = (e.head + 2) + 1 , tail = List/fold Natural e.tail (List Natural) (λ(x : Natural) → λ(y : List Natural) → [ (x + 2) + 1 ] # y) ([] : List Natural) } ```

Let me know if I forgot anything!