@psygnisfive I've added a brief note to the post...
-
-
Replying to @edwinbrady
@edwinbrady you should give some examples of what it means for Lazy to be ignored during totality checking1 reply 0 retweets 0 likes -
Replying to @beka_valentine
@psygnisfive I'm sure I should, but it's brief release notes, not documentation. It's for people to read quickly and see what's new.1 reply 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady fair point. i take it it means that youre not checking Lazy subterms for termination? but no loss of consistency because …2 replies 0 retweets 0 likes -
Replying to @beka_valentine
@edwinbrady …while Lazy Void might be provable, Void itself isn’t? that’s an interesting tack. i wonder the proof theoretic consequences1 reply 0 retweets 0 likes -
Replying to @beka_valentine
@psygnisfive By "ignored" I mean "elided". As if they were strict. Laziness in that sense is only meant as a performance thing.1 reply 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady ahh, ok, so its lazy evaluation with strict semantics, and its the type construct that’s ignored, not inhabitants. interesting1 reply 0 retweets 0 likes -
Replying to @beka_valentine
@edwinbrady is there a reason why lazy evaluation isnt employed uniformly, while retaining strict semantics?1 reply 0 retweets 0 likes -
Replying to @beka_valentine
@psygnisfive Yes. It's because I didn't want lazy evaluation...1 reply 0 retweets 0 likes -
@psygnisfive The lazy/strict discussion has been done to death. It's not something I want to get into. Except, perhaps, over beers :).
-
-
Replying to @edwinbrady
@edwinbrady ah. i have no horse in the race, or if i do, its on the eager side. im just curious about any design choice like that0 replies 0 retweets 0 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.