search

mbraceproject / FsPickler

A fast multi-format message serializer for .NET
http://mbraceproject.github.io/FsPickler/
MIT License
326 stars 52 forks source link

Experimental support for n-way sum types. #5

Closed t0yv0 closed 10 years ago

t0yv0 commented 10 years ago

Added sum types to the mix. Again, performance is dismal, but I am kind of happy I figured the types out.

I also finally have Coq code for these combinators without any undefined holes. As you see, they are very general, work in terms of binary pair, choice and wrap. My hope is that the Coq definition will help to:

  1. As we give it more structure to assume on Pickler<'T>, we can partially evaluate the definitions with that, automatically performing specialization.
  2. Semi-automatically unroll the definitions and compute efficient programs for the 2-3-4-5 cases.
  3. Figure out how to do rewriting simplifications.

I can share the Coq code if you are interested. Thanks.

eiriktsarpalis commented 10 years ago

Sure, go ahead. I suppose you have my email.

t0yv0 commented 10 years ago

I actually don't :) But here is the thing (sorry for cyptic variable names): https://gist.github.com/toyvo/6834822

eiriktsarpalis commented 10 years ago

Ah, saw you on my gtalk contacts and suspected you might have got it somehow.