Re: [racket-users] Question about Racket design philosophy: returning (void)
On 11 April 2018 at 06:48:49, Matthias Felleisen (matth...@felleisen.org) wrote: > Perhaps the real problem is one of the contract/type system. We have seen > effect systems > over and over again, though usually they try to express complicated > invariants and have > them checked at compile time. What if contract and type systems came with two > arrows: > > ->! for imperative functions, as in “this function may mutate the given > argument” > -> for ‘pure’ functions, as in “this function promises not to mutate the > given argument" I think this would be quite helpful. We can then easily enforce invariants like “the client-supplied function doesn’t mutate the given argument”. (Is there an existing way to enforce this?) On the other hand, I still like returning # for such imperative functions, because: (1) functionality-wise the returned value would be redundant; (2) for fluent DSLs, it could be ambiguous which input argument should be returned, and the best choice may depend on how the API is used in the client code. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Re: Question about Racket design philosophy: returning (void)
Racket's also flexible enough that you can say "to hell with void, I want function chaining" if you decide it's more appropriate: (require fancy-app) ;; now (+ _ 1) means (lambda (v) (+ v 1)) (require point-free) ;; now (~> x f g h) means (h (g (f x))) ;; makes voidful procedures return their argument (define ((action! proc) v) (proc v) v) ;; like ~>, but turns all procedures into actions first (define (act~> v . procs) (apply ~> v (map action! procs))) ;; voila! (act~> (make-vector 5) (vector-fill! _ 'blank) (vector-set! _ 2 'grapefruit) (vector-set! _ 0 'watermelon) (vector-map! symbol->string _) (vector-sort! _ stringhttps://groups.google.com/d/optout.
Re: [racket-users] Question about Racket design philosophy: returning (void)
Alexis says that (-> vector? exact-integer? any/c void?) is better than (-> vector? exact-integer? any/c vector?) because the former clearly signals the imperative nature of the function inside of the spec while the latter could be either a read-only or a RW function. Perhaps the real problem is one of the contract/type system. We have seen effect systems over and over again, though usually they try to express complicated invariants and have them checked at compile time. What if contract and type systems came with two arrows: ->! for imperative functions, as in “this function may mutate the given argument” -> for ‘pure’ functions, as in “this function promises not to mutate the given argument" but only in that they mutate a given argument. Then we could have both a ‘signal’ in the type/contract signature AND the “useful thing is returned” from Smalltalk (as Neil correctly reminds us). Of course, following my usual Laffer-curve-for-types argument, we should explore the usefulness of this idea with an inspection of existing code and other pragmatic explorations. ;; - - - [[ I think the idea of a fluent interface is a good one, but it doesn’t depend on OO and/or ‘self’ returns at all. We create fluently embedded DSLs in Racket all the time, and never touch either one of them. ]] -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Question about Racket design philosophy: returning (void)
Alexis King wrote on 04/10/2018 03:32 PM: There is definitely a school of thought that buys into the idea of returning “the thing being operated on” rather than returning nothing for side-effectful functions. I think this is most characterized by so-called “fluent interfaces”[1], a way of encoding DSLs into object-oriented languages. As far as I can tell, this was style has been around for a very long time, but it was really forced into mainstream usage by the runaway success of jQuery in the mid to late aughts. Yes, it was idiomatic in Smalltalk to return `self` for some things, and (together with the minimal required punctuation, the method names with interspersed arguments, and parsing disambiguation) this permitted the brave programmer to write neat-looking stream-of-words sequences of messages that jQuery could only dream of. :) In Racket, with the `racket/class` object system, you'd probably use `send*` instead, which is boring, but clear. BTW, Alexis is responding to the suggestion of "always return something useful, rather than void". I think the case of `gzip` without a second argument, however, is different. In that case, the code is generating a kind of handle or locator for the output of some (also side-effect-producing) operation. Given that this generation behavior has been put into this procedure, and that it is common for a program want to do something else with that output or its handle/locator, then I think it makes sense to return the generated locator. (`gzip` is not the best example, because it involves side effects in this other filesystem environment, along with locator naming conventions coming from elsewhere, which is why it can have the output argument unspecified.) -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Question about Racket design philosophy: returning (void)
> On Apr 10, 2018, at 14:00, David Storrs
> wrote:
>
> Aside from I/O, I can't think of too many cases where (void) is the
> intuitively correct or most useful return value, but it is extremely
> common throughout the built-in Racket functions. I'm not sure where
> you're drawing the lines on 'API design' vs 'comprehensive
> guidelines', but I'd sure like it if the guideline "Always return
> something useful unless there's a really good reason not to" got
> included.
There is definitely a school of thought that buys into the idea of
returning “the thing being operated on” rather than returning nothing
for side-effectful functions. I think this is most characterized by
so-called “fluent interfaces”[1], a way of encoding DSLs into
object-oriented languages. As far as I can tell, this was style has been
around for a very long time, but it was really forced into mainstream
usage by the runaway success of jQuery in the mid to late aughts.
The advantage of fluent interfaces is significant if you have an API
that involves frequent object creation and mutation. It makes it
possible to program in a more expression-oriented style, similar to the
way the GoF builder pattern is useful in C++/Java-style OO languages.
However, it has a cost of imprecision: it’s not always clear which thing
is the most obvious to return, and it masks when functions exist solely
for side-effects. For an example of the first problem, consider the
jQuery $.append function[2]:
$('.foo').append($('Hello!'))
Which element does this return? Does it return the set of elements
produced by $('.foo'), or does it return the new element created by
$('Hello!')? Both answers are useful, and indeed, jQuery actually
includes a separate $.appendTo function[3] that does the exact same
thing as $.append but flips the arguments around, mostly to make the
method chaining work out more nicely in certain situations. This is an
awkward thing for an API designer to worry about; it is confusing for a
library to provide the exact same function that just happens to return
a different one of its arguments.
The other problem with always returning something is that returning
# is extremely meaningful: it means the function’s only purpose
is to perform a side-effect. When contracts (or, in a statically typed
language, types) are used precisely, they can be quite communicative
without having to read anything but the signatures alone. When given a
Racket function with the following signature:
(-> vector? exact-integer? any/c void?)
...it’s pretty likely that function is vector-set!. But now imagine the
same function returned the mutated vector:
(-> vector? exact-integer? any/c vector?)
Now it’s much less immediately clear that this function is intended to
be used to perform a side-effect, and I might misinterpret it as
returning a new vector instead of updating the existing one.
You might argue that the benefit in chaining outweighs the cost of
signature clarity, but I think Racket mostly eschews that idea because
Racket is a language with a functional bent. It discourages using
mutability where immutable structures will do, and of course, useful
functions on immutable data cannot return #. Therefore, it’s both
(1) rare for idiomatic Racket to use lots of functions that produce
#, so they wouldn’t benefit much from threading arguments through,
and (2) especially important that side-effectful functions are called
out as such as efficiently as possible.
Racket makes it easy to use the same value twice without forcing library
authors to arbitrarily pick certain arguments to thread through
side-effectful functions. Internal definition contexts are available
almost everywhere, and there is a plethora of local binding forms.
Ultimately, the choice to return # instead of some input argument
probably doesn’t dramatically help or harm the language (it would still
be Racket if it aligned with the other school of thought), but I happen
to like the choice Racket makes.
Alexis
[1]: https://en.wikipedia.org/wiki/Fluent_interface
[2]: http://api.jquery.com/append/
[3]: http://api.jquery.com/appendTo/
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] Question about Racket design philosophy: returning (void)
On Tue, Apr 10, 2018 at 1:18 PM, Neil Van Dyke wrote: > Good catch; I agree that it would be better if `gzip` returned the target > path, in all cases. > > There is another change I'd make to that signature: currently, arg > `out-file` is optional, of type `path-string?`, defaulting to > `(path-add-extensionin-file".gz"#".")`. In a backward-compatible way, I'd > instead make it optional with type `(or/c #f path-string?)`, and defaulting > to `#f`, with an `#f` value then resulting in > `(path-add-extensionin-file".gz"#".")` behavior. That way, code calling > `gzip` can pass in the "use the default" value. This pattern becomes more > useful when there is more than one optional argument (whether or not it uses > keywords), but it's helpful even with just the one optional argument. It > also keeps the signatures in the documentation a little simpler. > > This might be getting into the "art" side of API design. We can come up > with some good stylistic guidelines for API design, probably including > guidelines that cover the above, but not comprehensive guidelines. Aside from I/O, I can't think of too many cases where (void) is the intuitively correct or most useful return value, but it is extremely common throughout the built-in Racket functions. I'm not sure where you're drawing the lines on 'API design' vs 'comprehensive guidelines', but I'd sure like it if the guideline "Always return something useful unless there's a really good reason not to" got included. Relatedly, the 'gunzip' function from file/gunzip (https://docs.racket-lang.org/file/gunzip.html) has this signature: (gunzip file [output-name-filter]) → void? file : path-string? output-name-filter : (string? boolean? . -> . path-string?) = (lambda (file archive-supplied?) file) This seems to be incorrect. The output-name-filter is getting a path? instead of a string? for its lead argument. Am I missing something? > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] IEEE 754 single precision float support
> > Then you probably want SIMD vector ops too, which, AFAIK, are not yet > supported. FP math in Racket does use the SIMD unit on most targets, > but normal math computes one value at a time, using only one slot per > SIMD register, as opposed to the N slots available at the given precision. > [This is the same as in C: if you want vector ops, you use SIMD > intrinsics instead of the normal C operators.] We already make heavy use of SIMD instructions in our main codebase, so I don't need Racket to do SIMD since I plan on only using Racket for offline analysis purposes. How long do you want to wait for "truth" calculations. Done using > either rationals (software bigint / bigint fractions), or bigfloats > (software adjustable width FP) with results converted to rational for > comparison, the truth calculation is going to be many orders of > magnitude slower than hardware FP math. > Do you have enough memory? Rationals can expand to fill all available > space. I can wait a while, but it can't be too slow, of course. If we're talking hours just to get a single computation done that involves just a handful of adds or multiplies, then this is untenable for me. But my experience shows that Racket is plenty fast for this simple case. Are there cases where it takes a surprising amount of extra time to perform a series of multiplies and adds? As for memory space, I have 32 GB of memory to spare. Should I be concerned with this when my computations typically only contain a few multiplies or adds? (FYI, it's not guaranteed that I'll restrict myself to such simple cases. We have many 4x4 matrix operations that we perform that I can definitely see myself looking into, some of which do orthonormalization or matrix inverses). Perhaps some kind of relative error measurement would be more > appropriate? Without knowing the algorithm in question, nobody can > really give better suggestions. Yes, for sure, but I currently only care about ULPs at the moment. -Dale Kim On Tuesday, April 10, 2018 at 1:48:16 AM UTC-7, gneuner2 wrote: > > > On 4/10/2018 1:36 AM, dk...@insomniacgames.com wrote: > > For the applications I work on, double precision floats are too costly > > to use; although the CPU cycle count to operate on doubles tend to be > > the same as single precision floats on modern hardware, the bandwidth > > cost is too prohibitive. We really do need single precision floats, > > and in many cases, 16 bit half precision floats due to the bandwidth > > savings. > > Then you probably want SIMD vector ops too, which, AFAIK, are not yet > supported. FP math in Racket does use the SIMD unit on most targets, > but normal math computes one value at a time, using only one slot per > SIMD register, as opposed to the N slots available at the given precision. > [This is the same as in C: if you want vector ops, you use SIMD > intrinsics instead of the normal C operators.] > > In Racket, there are tricks you can play with typed arrays and/or unsafe > operations to get more speed from bypassing the language's type > safeguards ... but you won't get vector ops AFAIK unless you drop into C > code. > > And again, there is no half precision available. Half precision is > available only in GPUs or certain DSPs - no CPU implements it. > > > > With regard to exactness, I don't need exactness to compare two single > > precision floats. I would like to have exactness in the ground truth > > that I compute to be able to calculate the error in the single > > precision float version of the computation. The idea is that I > > implement two versions of an algorithm. One uses the exact numbers > > supported by Racket and the other would use single precision floats, > > then I would like to compute error with (flulp-error x r) or something > > similar. > > How long do you want to wait for "truth" calculations. Done using > either rationals (software bigint / bigint fractions), or bigfloats > (software adjustable width FP) with results converted to rational for > comparison, the truth calculation is going to be many orders of > magnitude slower than hardware FP math. > > Do you have enough memory? Rationals can expand to fill all available > space. > > > > Is there a better approach to do this kind of analysis? > > You really haven't specified any "analysis" per se. Thus far you have > said only that you want to execute two versions of the same algorithm: > one using exact (or maybe high precision float) values, and one using > low (single) precision values, and compare the results. > > What you proposed is fine as far as it goes, but I question whether > measuring ulps error really is what you want to do. That more typically > would be done to compare answers computed to the same precision using > different algorithms. In your case, the low precision value will likely > lead to large errors vs the exact one - think about how intermediate > values overfl
Re: [racket-users] Question about Racket design philosophy: returning (void)
Good catch; I agree that it would be better if `gzip` returned the target path, in all cases. There is another change I'd make to that signature: currently, arg `out-file` is optional, of type `path-string?`, defaulting to `(path-add-extensionin-file".gz"#".")`. In a backward-compatible way, I'd instead make it optional with type `(or/c #f path-string?)`, and defaulting to `#f`, with an `#f` value then resulting in `(path-add-extensionin-file".gz"#".")` behavior. That way, code calling `gzip` can pass in the "use the default" value. This pattern becomes more useful when there is more than one optional argument (whether or not it uses keywords), but it's helpful even with just the one optional argument. It also keeps the signatures in the documentation a little simpler. This might be getting into the "art" side of API design. We can come up with some good stylistic guidelines for API design, probably including guidelines that cover the above, but not comprehensive guidelines. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Question about Racket design philosophy: returning (void)
A lot of functions in Racket return (void) instead of a useful value. One example is the gzip function from file/gzip; it would be useful if this returned the filepath to which the file was compressed, but instead it simply returns (void). I have a lot of respect for Racket and its designers, so I'm guessing this wasn't a random choice. What is the reason for this philosophy? -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] PLT Redex & dependent type
It is very helpful to me. You are so nice! Thank you very much! On Tuesday, April 10, 2018 at 9:35:31 PM UTC+8, William J. Bowman wrote: > > FYI, I have some other models here: > - A model of Luo's ECC, a much smaller model than CIC: > https://github.com/wilbowma/ecc-redex > - A couple of experimental models, including a model with just Π, and > failed attempt (IIRC) to model >Hoare Type Theory: https://github.com/wilbowma/dep-types-101 > > -- > William J. Bowman > > On Tue, Apr 10, 2018 at 07:53:37AM -0400, 'William J. Bowman' via Racket > Users wrote: > > Yes. https://github.com/wilbowma/cic-redex > > > > This isn't exactly a minimal example; I have a smaller model somewhere > I'll try to send. > > > > -- > > Sent from my phoneamajig > > > > > On Apr 10, 2018, at 06:32, Ning Shan > > wrote: > > > > > > Can I implement dependent type in PLT Redex? > https://en.wikipedia.org/wiki/Dependent_type > > > > > > Specifically Pi type. > > > > > > Can anyone give me a reference or a minimal example? Thanks in > advance. :-) > > > -- > > > You received this message because you are subscribed to the Google > Groups "Racket Users" group. > > > To unsubscribe from this group and stop receiving emails from it, send > an email to racket-users...@googlegroups.com . > > > For more options, visit https://groups.google.com/d/optout. > > > > -- > > You received this message because you are subscribed to the Google > Groups "Racket Users" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to racket-users...@googlegroups.com . > > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] PLT Redex & dependent type
FYI, I have some other models here: - A model of Luo's ECC, a much smaller model than CIC: https://github.com/wilbowma/ecc-redex - A couple of experimental models, including a model with just Π, and failed attempt (IIRC) to model Hoare Type Theory: https://github.com/wilbowma/dep-types-101 -- William J. Bowman On Tue, Apr 10, 2018 at 07:53:37AM -0400, 'William J. Bowman' via Racket Users wrote: > Yes. https://github.com/wilbowma/cic-redex > > This isn't exactly a minimal example; I have a smaller model somewhere I'll > try to send. > > -- > Sent from my phoneamajig > > > On Apr 10, 2018, at 06:32, Ning Shan wrote: > > > > Can I implement dependent type in PLT Redex? > > https://en.wikipedia.org/wiki/Dependent_type > > > > Specifically Pi type. > > > > Can anyone give me a reference or a minimal example? Thanks in advance. :-) > > -- > > You received this message because you are subscribed to the Google Groups > > "Racket Users" group. > > To unsubscribe from this group and stop receiving emails from it, send an > > email to racket-users+unsubscr...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] typed/racket surprises
On Mon, Apr 9, 2018 at 5:08 PM, Philip McGrath wrote: > Thanks for your helpful reply. I've created GitHub issues > https://github.com/racket/typed-racket/issues/691 and > https://github.com/racket/typed-racket/issues/692 to track the bugs, and I > will try my hand at a pull request for `parse-command-line` if I have time > before you do. Great, thanks! > On Fri, Apr 6, 2018 at 10:12 AM, Sam Tobin-Hochstadt > wrote: >> >> This is in some ways a weakness in the concept for `#:type-name`. The >> `struct` form relies on the parent struct to both find the type and to >> find the parent struct in the underlying `struct` macro. We could add >> a `#:parent-type-name` option to use here, but then we'd have to >> enforce that they go together in some way. I'm not sure what the best >> design is here. > > > This explanation makes sense—should something about this limitation be added > to the reference? Yes, it should -- or maybe `#:type-name` should behave like one of my workarounds. >> >> To work around this, try: >> >> #lang typed/racket >> (struct animal () #:transparent) >> (struct dog animal () #:transparent) >> (define-type Animal animal) > > > This seems like a very good work-around. Other than the fact that using > `#:type-name` would mean that `animal` could not be used as a type, is there > any difference between the result of this and what `#:type-name` does? That's the difference. > >> >> > 3. parse-command-line doesn't support usage-help, help-labels, >> > help-proc, or >> > unknown-proc > > > A part of this that particularly surprised me was that the built-in type > didn't work with `require/typed` because Typed Racket couldn't generate a > contract for it. Is the generation of contracts for built-in types handled > differently than for programmer-specified types? Yes, it's quite different -- Typed Racket doesn't actually generate a contract for `parse-command-line` (or for other built-in functions like `+` or `list`). > More broadly, I don't feel like I have very strong intuitions about what > types Typed Racket can and can't generate contracts for. I believe the Typed > Racket team is working to be able to generate contracts for more and more > types, so maybe you are avoiding specifics in the documentation for that > reason, but I think it would be valuable to have some more detail about what > is currently possible. Yes, I think more documentation on this would be an improvement. This section has a bit of that http://docs.racket-lang.org/ts-guide/caveats.html but we should add more. The part that doesn't work is the type for `finish-proc`, which uses `...` in the type in a way that Typed Racket can't automatically generate a contract for. Sam -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Re: error in DrRacket but not in script
Yes, that's that ! Many thanks, also for providing the suggestion. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Re: error in DrRacket but not in script
My guess the problem is (define imleftname #"./tsukubaleft.jpg") You're using a relative path to the jpg file which may be valid wherever your script file is located but DrRacket is probably starting up with a different working directory and the relative path is not resolving successfully. I would suggest trying using `define-runtime-path` which deals with that kind of issue. It will automatically create the correct fully resolved path when you give it a relative path. For example, do it like this: (define-runtime-path imleftname "./tsukubaleft.jpg") On Tuesday, April 10, 2018 at 4:38:12 AM UTC-4, Frédéric Morain-Nicolier wrote: > > Hello, > > I'm just a beginner in Racket and want to use the opencv bindings. I have > this small basic code : > > #! /usr/bin/env racket > #lang racket/base > > (require > opencv/highgui) > > ; lecture des deux images et affichage (pour tester) > > (define imleftname > #"./tsukubaleft.jpg") > > (define im-left (imread imleftname CV_LOAD_IMAGE_COLOR)) > (imshow "Display window" im-left) > (define key (cvWaitKey 0)) > (exit 0) > > The execution from the shell is ok but when executing it in the DrRacket > console I get this error on (imread imleftname CV_LOAD_IMAGE_COLOR) : > > ptr-ref: contract violation > expected: (and/c cpointer? (not/c (lambda (p) (pointer-equal? p #f > given: #f > argument position: 1st > other arguments...: ># > > Thanks for your help in advance to understand, > Frédéric > > > > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] Re: [racket] Dr. Racket for iOS
Has this been looked into again? Especially now that we have Swift playgrounds and the iPad Pro. The iPad Pro would be my pc if only it had a racket/scheme programming environment. I’ve found a few gambit is no longer kept up to date meaning it’s not optimized for the Pro and iOS 11. I firmly believe either this year or next we will see Xcode on the iPad and it would be a shame not to have lisp as well. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] PLT Redex & dependent type
Yes. https://github.com/wilbowma/cic-redex This isn't exactly a minimal example; I have a smaller model somewhere I'll try to send. -- Sent from my phoneamajig > On Apr 10, 2018, at 06:32, Ning Shan wrote: > > Can I implement dependent type in PLT Redex? > https://en.wikipedia.org/wiki/Dependent_type > > Specifically Pi type. > > Can anyone give me a reference or a minimal example? Thanks in advance. :-) > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] PLT Redex & dependent type
Can I implement dependent type in PLT Redex? https://en.wikipedia.org/wiki/Dependent_type Specifically Pi type. Can anyone give me a reference or a minimal example? Thanks in advance. :-) -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] IEEE 754 single precision float support
On 4/10/2018 1:36 AM, d...@insomniacgames.com wrote: For the applications I work on, double precision floats are too costly to use; although the CPU cycle count to operate on doubles tend to be the same as single precision floats on modern hardware, the bandwidth cost is too prohibitive. We really do need single precision floats, and in many cases, 16 bit half precision floats due to the bandwidth savings. Then you probably want SIMD vector ops too, which, AFAIK, are not yet supported. FP math in Racket does use the SIMD unit on most targets, but normal math computes one value at a time, using only one slot per SIMD register, as opposed to the N slots available at the given precision. [This is the same as in C: if you want vector ops, you use SIMD intrinsics instead of the normal C operators.] In Racket, there are tricks you can play with typed arrays and/or unsafe operations to get more speed from bypassing the language's type safeguards ... but you won't get vector ops AFAIK unless you drop into C code. And again, there is no half precision available. Half precision is available only in GPUs or certain DSPs - no CPU implements it. With regard to exactness, I don't need exactness to compare two single precision floats. I would like to have exactness in the ground truth that I compute to be able to calculate the error in the single precision float version of the computation. The idea is that I implement two versions of an algorithm. One uses the exact numbers supported by Racket and the other would use single precision floats, then I would like to compute error with (flulp-error x r) or something similar. How long do you want to wait for "truth" calculations. Done using either rationals (software bigint / bigint fractions), or bigfloats (software adjustable width FP) with results converted to rational for comparison, the truth calculation is going to be many orders of magnitude slower than hardware FP math. Do you have enough memory? Rationals can expand to fill all available space. Is there a better approach to do this kind of analysis? You really haven't specified any "analysis" per se. Thus far you have said only that you want to execute two versions of the same algorithm: one using exact (or maybe high precision float) values, and one using low (single) precision values, and compare the results. What you proposed is fine as far as it goes, but I question whether measuring ulps error really is what you want to do. That more typically would be done to compare answers computed to the same precision using different algorithms. In your case, the low precision value will likely lead to large errors vs the exact one - think about how intermediate values overflowing or underflowing might affect the end result. Perhaps some kind of relative error measurement would be more appropriate? Without knowing the algorithm in question, nobody can really give better suggestions. -Dale Kim YMMV, George -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[racket-users] error in DrRacket but not in script
Hello, I'm just a beginner in Racket and want to use the opencv bindings. I have this small basic code : #! /usr/bin/env racket #lang racket/base (require opencv/highgui) ; lecture des deux images et affichage (pour tester) (define imleftname #"./tsukubaleft.jpg") (define im-left (imread imleftname CV_LOAD_IMAGE_COLOR)) (imshow "Display window" im-left) (define key (cvWaitKey 0)) (exit 0) The execution from the shell is ok but when executing it in the DrRacket console I get this error on (imread imleftname CV_LOAD_IMAGE_COLOR) : ptr-ref: contract violation expected: (and/c cpointer? (not/c (lambda (p) (pointer-equal? p #f given: #f argument position: 1st other arguments...: # Thanks for your help in advance to understand, Frédéric -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
