I’ve just merged this. What could possibly go wrong, after all? Documentation is currently TL;DW but might happen later if things work out.https://twitter.com/edwinbrady/status/810622505052467202 …
You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
I’ve just merged this. What could possibly go wrong, after all? Documentation is currently TL;DW but might happen later if things work out.https://twitter.com/edwinbrady/status/810622505052467202 …
Interesting! why does mCons take 'xs' and ignores it? Is it related to the linear typing?
the 0 in the binder means it's only interesting at the type level and not a thing to be inspected at run time
could someone provide a link to the paper or other explanation? Interested here, but clueless.
It’s a bit of a teaser, but based on @pigworker’s https://personal.cis.strath.ac.uk/conor.mcbride/pub/Rig.pdf … (can’t find the published version online just now, alas)
→ (1 x : a) → (1 xs : List a) → encodes tensor, x ⊗ xs, how'd you encode with: x & xs. I missed that from the conors paper...
I’ve missed that too. For my current purposes it’s not so important, but I’d like to know the answer…
can you do with or par? I know a way :)
There’s some fairly basic things I still can’t do…
Is this based on @pigworker's paper on this sort of thing?
Those are the rules I'm playing with, yes @pigworker
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.