tweag / linear-types

Drafts, notes and resources for adding linear typing to GHC.
75 stars 5 forks source link

Proposed experiment - build stackage with some linear prelude types #8

Open rrnewton opened 7 years ago

rrnewton commented 7 years ago

How to show that a linear extension is backwards compatible? One way to substantiate that claim is to actually build large amounts of code with it.

I.e. if we replace the type of (++) in the prelude, does all of stackage still build?

This experiment is so simple that maybe we can even do it for this submission.

aspiwack commented 7 years ago

Almost certainly not, unfortunately. There will be a need of eta-expanding the function here and there.

Of course we can do

(++') :: [a] -o [a] -o [a]
(++) :: [a] -> [a] -> [a]
a ++ b = a ++' b

Which proves, at least, that we can have both types hanging about with minimal boilerplate.

rrnewton commented 7 years ago

Oh, that's too bad.... what about something smaller. What about building nofib?

aspiwack commented 7 years ago

So building base and nofib? There will probably be a few eta-expansions to do along the way. Would that be acceptable? If so, then yes, we could do it.

rrnewton commented 7 years ago

Sure! I think it still sounds somewhat convincing -- we build N lines of legacy code where N is in the thousands!