[racket] Typed Racket frustration

On Jan 24, 2015, at 1:43 AM, Matthew Butterick wrote:

> FWIW, Sam's point that one can't expect every untyped program to work without modification is entirely fair.

Correct. 

> But Konrad's point is also fair: if a function like `append` or `hash` works differently in TR, then it is, for practical purposes, not the same function, even if it relies on the same code.

This statement is too coarse. There are at least two senses in which a TR function f is distinct from an R function: 

1. f's type restricts the usability of f to a strict "subset" [in the naive set-theoretic sense]. This is most likely due to a weakness of the type system; the language of "theorems" isn't strong enough to express R's intention w/o making the inference rules unsound. [Unlike in the legal world, In PL arguments of 'typedness' must be about truly-guilty or not-guilty. The rulings are completely impartial and uniform, i.e., totally fair.]

2. f's type ___changes___ the meaning of the code. (That's also possible but I don't want to fan the argument that Sam and I have about this.) 


> If it would be superfluous to repeat every TR function in the documentation, it still could be valuable to document some of the major departures from Racket. I mean, I would read that, for sure ;)


Actually it would not be superfluous. We just don't have the manpower but perhaps it's time to tackle this problem (perhaps in a semi-automated manner). 

-- Matthias

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20150124/ac77287c/attachment.html>