Skip to content

6 Open-Servers

  • 6.2 fix the Servant DSL ⏫
    • NOTE: After the changes to the core, the Servant examples won't work anymore
    • issue #34
  • 6.5 try out idris-server http server project ✅ 2022-03-14
    • 6.5.1 run locally -- doesn't work ✅ 2021-11-10
    • 6.5.2 Perform the suggested fixes from discord ✅ 2021-11-11
    • NOTE: didn't work, missing module: TyTTP.Support.Promise
    • 6.5.2' Perform the suggested fixes from discord ✅ 2022-03-14
    • NOTE: Updated info from package author, need to try again!
    • 6.5.3 see if we can interpret LogIO into the node JS server ✅ 2022-03-14
    • looks like this is not what we are looking for, the Tyttp library is too high level and the prototype diverged too much from Recombine
  • [-] ~~6.7 Try out new lenses~~
    • [-] ~~6.7.1 try the dependent van-laarhoven~~
    • Functor f => ((i : a) -> {0 b : a -> Type} -> f (b i)) -> (i : s) -> {0 t : s -> Type} -> f (t i)
  • ~~6.8 dependent lenses are morphisms between containers. Comonads are morphisms between directed containers. Can we convert from one to the other?~~
    • Note: they are not directed containers but database might be
  • 6.9 Refactor the PathComp Datatype do get rid of Str constructor and use product and sum ✅ 2022-03-27 and String.Singleton instead
    • 6.9.1 remove the use of Product and Sum and replace it with a custom type with suitable ✅ 2022-03-27 parsing functions
  • 6.11 Take a look at Matteo's draft of the paper ✅ 2022-02-17
  • 6.12 Allow dependent endpoints ⏫ ✅ 2022-03-14
    • We do not need this anymore
  • 6.13 Tensor in the DSL ⏫ ✅ 2022-02-17
    • 6.13.1 Finish writing the tensor examples ✅ 2022-02-17
  • 6.14 Port indexed interfaces to container interfaces ✅ 2022-03-14
    • Not going to work, it messes up inference
  • 6.15 implement state as action ✅ 2022-03-27
    • issue #44
  • 6.16 implement servers as bidirectional lenses for each endpoints ✅ 2022-03-27
    • issue #42
  • 6.17 finish database example
    • BLOCKED: Need to deal with 6.18 first
  • 6.18 add error management with co-parameter
    • 6.18.1 Implement co-para lenses ✅ 2022-04-13
    • 6.18.2 Implement para and co-para lenses ✅ 2022-04-13
    • 6.18.3 Implement errors on the backward part
  • 6.19 implement server communication with node ✅ 2022-04-13
  • 6.20 Implement authentication and caching
    • 6.20.1 Implement + for Indexed containers ✅ 2022-04-13
    • 6.20.2 Implement "my" indexed containers as a container with a unit parameter
    • 6.20.3 Implement caching with + on the output
  • 6.21 Write definition of server composition language on paper ✅ 2022-07-12
    • 6.21.1 Implement the dependently typed language using terms ✅ 2022-07-12
  • 6.22 Write lenses as update monads and see if we can track effects ✅ 2022-05-19
    • NOTE: composition does not work
  • 6.23 Find monoidal structures on Suspended containers ✅ 2022-07-12
    • It's not a category because there is no identity on containers
  • 6.24 Find a unifying structure for bidirectional servers
    • 6.24.1 embedd resource lenses into it
    • 6.24.2 embed cache middle ware
    • 6.24.3 embed authentication middleware