Re: [racket-dev] typed racket non-monotonic in scary way?
On 09/07/2012 06:42 PM, John Clements wrote: I was trying to write a function on natural numbers today, and came up with an example that scares me all to bits. This program: #lang typed/racket (: int->nat (Natural -> Natural)) (define (int->nat n) (cond [(<= n 0) 13] [else (- n 1)])) Does not type-check, because (- n 1) has type Integer rather than Natural. Well, too bad, but sort of okay. But then: #lang typed/racket (: int->nat (Integer -> Natural)) (define (int->nat n) (cond [(<= n 0) 13] [else (- n 1)])) *does* typecheck. AIIEE! As far as I can tell, Integer is a supertype of Natural, so I would expect that things that typecheck with Integer inputs should also typecheck with Natural inputs. Please please tell me this is a bug? I can imagine a world where it's not a bug, but the difficulty of using the type system would skyrocket if you have to consider *widening* types as well as narrowing them to get things to work. No? I'd report it. The filters on the types of functions like `<=' are axioms in the type system. Adding such axioms in a way that invalidates the type system's properties should be regarded as an error. FWIW, the filters on predicates are more likely to be correct because their huge `case->' types are less huge. For example, the filter for `positive?' doesn't seem to make the type system non-monotone: (: int->nat (Natural -> Natural)) (define (int->nat n) (cond [(not (positive? n)) 13] [else (- n 1)])) This typechecks just fine. There should be a way to catch this kind of thing with randomized testing, or (less likely) by analyzing the `case->' types. Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
[racket-dev] typed racket non-monotonic in scary way?
I was trying to write a function on natural numbers today, and came up with an example that scares me all to bits. This program: #lang typed/racket (: int->nat (Natural -> Natural)) (define (int->nat n) (cond [(<= n 0) 13] [else (- n 1)])) Does not type-check, because (- n 1) has type Integer rather than Natural. Well, too bad, but sort of okay. But then: #lang typed/racket (: int->nat (Integer -> Natural)) (define (int->nat n) (cond [(<= n 0) 13] [else (- n 1)])) *does* typecheck. AIIEE! As far as I can tell, Integer is a supertype of Natural, so I would expect that things that typecheck with Integer inputs should also typecheck with Natural inputs. Please please tell me this is a bug? I can imagine a world where it's not a bug, but the difficulty of using the type system would skyrocket if you have to consider *widening* types as well as narrowing them to get things to work. No? John smime.p7s Description: S/MIME cryptographic signature _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] racket/format
The change to ~a, ~v, and ~s seems reasonable to me. The renamed
keywords and generalization of ~v and ~s to multiple arguments are good.
The ~r function seems okay except for the way it chooses which notation
(positional or exponential) to use. It should take a rule, not an
answer, and the default rule should not depend on the precision
argument, as it produces peculiar results. Contrast:
(catn pi #:precision 0) = "3"
(~r pi #:precision 0) = "3e+00"
Unfortunately, I think the kind of rules supported by 'catn'
(pos/exp-range) are also wrong. Probably the best solution is to take a
function. I'll change ~r to drop the #:exponential? argument and instead
take a #:notation argument, with contract
(or/c 'positional 'exponential
(-> rational? (or/c 'positional 'exponential)))
and default value of 'positional.
Ryan
On 09/07/2012 10:27 AM, Matthew Flatt wrote:
I've added a `racket/format' library that is a revised version of
Ryan's `unstable/cat'. It's re-exported by `racket', but not by
`racket/base'.
I think Ryan's library is a step in the right direction for string
formatting, and the difficult remaining task is getting the names
right. So, this `racket/format' experiment changes all of the names.
As reflected in the `racket/format' library name, the new function
names are intended to leverage your experience with `format': the `cat'
function is `~a', the `catp' function is `~v', and the `catw' function
is `~s'. The `catn' functions are collapsed to a single `~r'.
Using this library, instead of writing
(format "The result of\n ~s\nis\n ~v"
expr
(eval expr))
you'd write
(~a "The result of\n"
" " (~s expr) "\n"
"is\n"
" " (~v (eval expr)))
or even, when using `#lang at-exp racket',
@~a{The result of
@~s[expr]
is
@~v[(eval expr)]}
Keyword options like `#:width' and `#:align', of course, can be an even
bigger help for formatting.
I concede that names like `~s' are not remotely mnemonic unless you've
already learned the somewhat obscure `format' escapes, but it seems
difficult to find compact names that are meaningful and that don't
cause collisions; we can at least take advantage of the compact names
that we've already learned. Embracing tildes also means that we worry
less about replacing all sorts of APIs, such as `error', that have
`format' built in. And maybe `~a' works relatively well as a shorthand
for `string-append'.
_
Racket Developers list:
http://lists.racket-lang.org/dev
_
Racket Developers list:
http://lists.racket-lang.org/dev
[racket-dev] racket/format
I've added a `racket/format' library that is a revised version of
Ryan's `unstable/cat'. It's re-exported by `racket', but not by
`racket/base'.
I think Ryan's library is a step in the right direction for string
formatting, and the difficult remaining task is getting the names
right. So, this `racket/format' experiment changes all of the names.
As reflected in the `racket/format' library name, the new function
names are intended to leverage your experience with `format': the `cat'
function is `~a', the `catp' function is `~v', and the `catw' function
is `~s'. The `catn' functions are collapsed to a single `~r'.
Using this library, instead of writing
(format "The result of\n ~s\nis\n ~v"
expr
(eval expr))
you'd write
(~a "The result of\n"
" " (~s expr) "\n"
"is\n"
" " (~v (eval expr)))
or even, when using `#lang at-exp racket',
@~a{The result of
@~s[expr]
is
@~v[(eval expr)]}
Keyword options like `#:width' and `#:align', of course, can be an even
bigger help for formatting.
I concede that names like `~s' are not remotely mnemonic unless you've
already learned the somewhat obscure `format' escapes, but it seems
difficult to find compact names that are meaningful and that don't
cause collisions; we can at least take advantage of the compact names
that we've already learned. Embracing tildes also means that we worry
less about replacing all sorts of APIs, such as `error', that have
`format' built in. And maybe `~a' works relatively well as a shorthand
for `string-append'.
_
Racket Developers list:
http://lists.racket-lang.org/dev
