4 ms·
Lean doesn’t have any kind of substructural typing, does it? At a glance it looks like you need to manually (lexically) rebind the socket at each step in the op
by wk_end 7mo ago
Lean doesn’t have any kind of substructural typing, does it? At a glance it looks like you need to manually (lexically) rebind the socket at each step in the operation, and there’s nothing stopping you from holding onto a socket in a now-invalid state and making mess of things, right?
Also, boo AI slop. If you’re going to use AI to help write your technical blog posts please please please edit out all the “No X. No Y. Just pure Z.” marketing-speak.
- tczMUFlmoNk 7mo agoThis is what I was thinking, too. Without some kind of linearity, `connect` et al. don't give the claimed guarantees if you can just reuse the old socket handle. Especially if it's aliased in a list or something. I was surprised to see this not mentioned at all in the section specifically dedicated to double-close prevention. Likewise, with implicit weakening, nothing stops you from dropping the socket without closing it.
- ngrislain 7mo agoYes the user has to be cooperative somehow. You could emulate linear/affine types like features with indexed monads though.