Brendan Zabarauskas on Twitter

This Tweet is from a suspended account. Learn more

Aug 13, 2018

I've always felt TC, while having desirable theoretical properties, was not representative of physical reality, and found concepts like en.wikipedia.org/wiki/Linear_bo much more compelling. But I'm torn between the beauty of, say, inductive Nat, vs a more bounded (Fin-like?) type.

en.wikipedia.org

Linear bounded automaton - Wikipedia

2

1

ᵉᵈᵈʸᵇ

@eddyb_r

Aug 13, 2018

I was going to say something about Pola and ask if you know of similar exciting developments but all I can find is researchgate.net/profile/Robin_ - I could swear I saw something like a full-blown thesis about it, a while back

2

This Tweet is from a suspended account. Learn more

ᵉᵈᵈʸᵇ

@eddyb_r

Aug 13, 2018

Ohhh, using linear types to limit the space usage, that's a neat trick! Come to think of it, that feels a lot like Rust (with `T -> T` functions or `&mut T` in-place mutation). Then again, we also sometimes build linked lists on the stack by recursion "for fun" (and profit) :P.

1

ᵉᵈᵈʸᵇ

@eddyb_r

Aug 13, 2018

*a lot like Rust without dynamic allocation - which is somewhat easier to avoid because you have to go through certain types to get it in the first place. I really wish sometimes I had something in-between, where I'd get dynamic allocations for recursive ADTs automatically.

1

ᵉᵈᵈʸᵇ

@eddyb_r

Aug 13, 2018

(great, now I'm just spamming this thread with my half-baked rants about somewhat magical PLs :P. in truth, one tool for all the jobs would be quite the feat to even conceive, let alone implement)

1

Replying to

and

Sort of related, but I've been thinking of trying to get something where multiplicity > 1 implies some that you need some sort of allocator (ie. in something like

@bentnib

&

@lamudri

's bentnib.org/context-constr). But I want that to be configurable. Ugh, it's a hard problem.

8:16 AM · Aug 13, 2018Twitter Web Client

Replying to

Ie. I want to be able to specify a GC or arena or whatever. And also be able to do something about OOM. All of this kind of needs some interaction between coeffects and effects though, which is well beyond me. And then you get tons of coeffect/effect annotations eeverywhere.

1

James Wood

@laMudri

Aug 13, 2018

Semantic results really should inform the compiler more. I'm not sure what Idris (Blodwen?) does, but I imagine resource information gets erased.

1

Show replies

Conversation