3 ms·

How can linear types be used for something like doing a bunch of calculations on a DataFrame of unknown size ? ex: filter rows based on certain conditions, comp

How can linear types be used for something like doing a bunch of calculations on a DataFrame of unknown size ? ex: filter rows based on certain conditions, compute some averages, and then plot certain columns etc. Its hard to find real world use examples and learn about linear types when I search online. If anyone has links, that would help.

whateveracct 6y ago
They'd mostly be used for creating a pure API around any mutability under the hood But we already had ST for that, so the real advantage of LTs over ST is you can type-safely "freeze" and "thaw" your mutable structure without copying. The mutable array example in the Linear Haskell paper is a simple comparison to what you're asking for.
jose_zap 6y ago
Some real world examples with links: - A safe streaming library where effects are guaranteed to only be performed once: https://www.tweag.io/blog/2018-06-21-linear-streams/ https://www.tweag.io/blog/2018-06-21-linear-streams/ - Efficient zero-copy network communication: https://www.tweag.io/blog/2017-08-24-linear-types-packed-data/ https://www.tweag.io/blog/2017-08-24-linear-types-packed-dat... - Safe manual memory management and prompt resource release: https://www.tweag.io/blog/2020-02-06-safe-inline-java/ https://www.tweag.io/blog/2020-02-06-safe-inline-java/ - Explicit API design to guide developers on what function to call next when implementing a protocol like TCP: https://www.tweag.io/blog/2017-08-03-linear-typestates/ https://www.tweag.io/blog/2017-08-03-linear-typestates/ - Add correctness proofs to already existing algorithm implementations like merge sort: https://www.tweag.io/blog/2018-03-08-linear-sort/ https://www.tweag.io/blog/2018-03-08-linear-sort/
- vsskanth 6y ago
  Thank you!
taktoa 6y ago
It's not "linear" as in linear algebra (well, it is technically, but only in the abstruse sense that the category of the vector spaces and linear maps is a model of linear logic).

whateveracct 6y ago

They'd mostly be used for creating a pure API around any mutability under the hood But we already had ST for that, so the real advantage of LTs over ST is you can type-safely "freeze" and "thaw" your mutable structure without copying. The mutable array example in the Linear Haskell paper is a simple comparison to what you're asking for.

jose_zap 6y ago

Some real world examples with links: - A safe streaming library where effects are guaranteed to only be performed once: https://www.tweag.io/blog/2018-06-21-linear-streams/ https://www.tweag.io/blog/2018-06-21-linear-streams/ - Efficient zero-copy network communication: https://www.tweag.io/blog/2017-08-24-linear-types-packed-data/ https://www.tweag.io/blog/2017-08-24-linear-types-packed-dat... - Safe manual memory management and prompt resource release: https://www.tweag.io/blog/2020-02-06-safe-inline-java/ https://www.tweag.io/blog/2020-02-06-safe-inline-java/ - Explicit API design to guide developers on what function to call next when implementing a protocol like TCP: https://www.tweag.io/blog/2017-08-03-linear-typestates/ https://www.tweag.io/blog/2017-08-03-linear-typestates/ - Add correctness proofs to already existing algorithm implementations like merge sort: https://www.tweag.io/blog/2018-03-08-linear-sort/ https://www.tweag.io/blog/2018-03-08-linear-sort/

vsskanth 6y ago
Thank you!

taktoa 6y ago

It's not "linear" as in linear algebra (well, it is technically, but only in the abstruse sense that the category of the vector spaces and linear maps is a model of linear logic).