I wish people would stop using length-indexed vectors as the canonical example of dependent types.
@psnively @copumpkin what do you suggest instead? I agree, it's boring, but it's easy to get the point quickly.
-
-
@edwinbrady@psnively@copumpkin Packets with several length fields that must agree, perhaps? -
@sergeybratus@psnively@copumpkin I think that needs to be a follow up. Something familiar is good for getting used to syntax. - 1 more reply
New conversation -
-
-
@edwinbrady@psnively@copumpkin which aren't outside the ken of Human skills. Examples that are hard for people to do otherwise = magic -
@cartazio@psnively@copumpkin it is important to remember that people reading these examples often aren't aware that even that is possible. - 7 more replies
New conversation -
-
-
@edwinbrady@psnively@copumpkin true, but it's info that just makes head a total function and makes it safe to do unchecked indexingThanks. 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.