Re: [racket-users] Gradual Typed Racket?

2020-04-17 Thread Marc Kaufmann 
Fantastic, thanks for the clarification Ben. I'll start using it to see
what it does, as I have a few functions that occasionally throw errors
through contracts - which I should call 'blame' - yet I can't figure out
much from it.

On Fri, Apr 17, 2020 at 6:09 PM Ben Greenman 
wrote:

> On 4/17/20, Sorawee Porncharoenwase  wrote:
> >>
> >> My understanding is that contract-out only provides protection against
> >> inappropriate calls from clients *outside* the module, whereas
> >> define/contract enforces the contract against everyone, including things
> >> inside the module.  Do I have that right?
> >>
> >
> > I think that's correct. Note though that the implication is that
> > define/contract could produce a much more expensive code, especially for
> > recursive function, since it will need to check against the contract for
> > every iteration.
> >
> >
> >> On a related topic, I don't understand the concept of positive and
> >> negative blame.  Can someone fill me in?
> >>
> >
> > I always forget which is positive and negative, so I won't use the terms
> > here (and too lazy to lookup). But roughly, suppose you attach a function
> > contract (-> number? string?) to a function value, then there are mainly
> > two ways things could go wrong.
> >
> > 1. Client uses the function incorrectly by calling it with non-number.
> > 2. The function itself returns a non-string.
> >
> > A blame would indicate whose party is at fault when a contract is
> > violated--caller or the function itself.
>
> 1 = negative = the client that uses the value
> 2 = positive = the code that made the value
>
> But unless you're using `contract` directly, you don't need to know
> these words to benefit from contracts.
>
> --
> You received this message because you are subscribed to a topic in the
> Google Groups "Racket Users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/racket-users/VA_ufNV6J24/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
> racket-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/CAFUu9R5vabY64_HZRWv1zNoyuEd7K5p8i8jfVN0JB1reufYEPw%40mail.gmail.com
> .
>

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAD7_NO7Yo%2BL-T5JnxKB74-OPNce3On0YY%3DujHLR7L%2B1Ch%2Bqz1w%40mail.gmail.com.

Re: [racket-users] Gradual Typed Racket?

2020-04-17 Thread Ben Greenman 
On 4/17/20, Sorawee Porncharoenwase  wrote:
>>
>> My understanding is that contract-out only provides protection against
>> inappropriate calls from clients *outside* the module, whereas
>> define/contract enforces the contract against everyone, including things
>> inside the module.  Do I have that right?
>>
>
> I think that's correct. Note though that the implication is that
> define/contract could produce a much more expensive code, especially for
> recursive function, since it will need to check against the contract for
> every iteration.
>
>
>> On a related topic, I don't understand the concept of positive and
>> negative blame.  Can someone fill me in?
>>
>
> I always forget which is positive and negative, so I won't use the terms
> here (and too lazy to lookup). But roughly, suppose you attach a function
> contract (-> number? string?) to a function value, then there are mainly
> two ways things could go wrong.
>
> 1. Client uses the function incorrectly by calling it with non-number.
> 2. The function itself returns a non-string.
>
> A blame would indicate whose party is at fault when a contract is
> violated--caller or the function itself.

1 = negative = the client that uses the value
2 = positive = the code that made the value

But unless you're using `contract` directly, you don't need to know
these words to benefit from contracts.

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAFUu9R5vabY64_HZRWv1zNoyuEd7K5p8i8jfVN0JB1reufYEPw%40mail.gmail.com.

Re: [racket-users] Gradual Typed Racket?

2020-04-17 Thread Sorawee Porncharoenwase 
>
> My understanding is that contract-out only provides protection against
> inappropriate calls from clients *outside* the module, whereas
> define/contract enforces the contract against everyone, including things
> inside the module.  Do I have that right?
>

I think that's correct. Note though that the implication is that
define/contract could produce a much more expensive code, especially for
recursive function, since it will need to check against the contract for
every iteration.


> On a related topic, I don't understand the concept of positive and
> negative blame.  Can someone fill me in?
>

I always forget which is positive and negative, so I won't use the terms
here (and too lazy to lookup). But roughly, suppose you attach a function
contract (-> number? string?) to a function value, then there are mainly
two ways things could go wrong.

1. Client uses the function incorrectly by calling it with non-number.
2. The function itself returns a non-string.

A blame would indicate whose party is at fault when a contract is
violated--caller or the function itself.


>
>
>> Here's an example to play with. Submod A provides two functions: f0 is
>> made with define/contract and f1 with contract-out.
>>
>> ```
>>   #lang racket
>>
>>   (module A racket
>> (define/contract (f0 x)
>>   (-> natural? natural?)
>>   x)
>>
>> (define (f1 x)
>>   x)
>>
>> (provide f0)
>> (provide (contract-out [f1 (-> natural? natural?)])))
>>
>>   (module B racket
>> (require (submod ".." A))
>> (f0 'hello)
>> #;(f1 'hello))
>>
>>   (require 'B)
>> ```
>>
>> If B makes a mistake with f0, the error blames submod A.
>> But if B makes a mistake with f1, the error blames B.
>>
>>
>> The contract library makes these blame errors internally. I don't
>> think there's any way to customize short of using `contract` directly.
>>
>> > Is it related to this part of the documentation of `contract-out`
>> > (
>> https://docs.racket-lang.org/reference/attaching-contracts-to-values.html#%28form._%28%28lib._racket%2Fcontract%2Fbase..rkt%29._contract-out%29%29
>> )
>> > - which I admittedly don't understand:
>> >
>> > "The implementation of contract-out
>> > <
>> https://docs.racket-lang.org/reference/attaching-contracts-to-values.html#%28form._%28%28lib._racket%2Fcontract%2Fbase..rkt%29._contract-out%29%29
>> >
>> > uses syntax-property
>> > <
>> https://docs.racket-lang.org/reference/stxprops.html#%28def._%28%28quote._~23~25kernel%29._syntax-property%29%29
>> >
>> > to attach properties to the code it generates that records the syntax of
>> > the contracts in the fully expanded program. Specifically, the symbol '
>> > provide/contract-original-contract is bound to vectors of two elements,
>> the
>> > exported identifier and a syntax object for the expression that produces
>> > the contract controlling the export."
>>
>> I was only thinking of the "blaming: " part of error messages.
>>
>> Both define/contract and contract-out can print the whole contract; I
>> don't think this syntax-property gives contract-out any advantage
>>
>> (Sadly, the whole contract is sometimes too big to help me find a
>> problem.)
>>
>> --
>> 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.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/racket-users/CAFUu9R5BMG5ZFVrddrJ-6uceV%2B3936ZudE-8ESObycw9B%2BRjcg%40mail.gmail.com
>> .
>>
> --
> 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.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/CAE8gKof2M%2BHuCf%2B2hfTKbVxCxGEb1Vtx%2BaXehYNZXhttpgMNPA%40mail.gmail.com
> 
> .
>

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CADcuegskOV0cOQ8xYjTmbED2XA8dvZj9OkY_aFP0_7d28Lho3g%40mail.gmail.com.

Re: [racket-users] Gradual Typed Racket?

2020-04-17 Thread David Storrs 
On Fri, Apr 17, 2020 at 9:45 AM Ben Greenman 
wrote:

> Hi Marc,
>
>
> >> For contracts, though, (provide (contract-out ...)) gives better error
> >> messages than define/contract.
> >>
> >
> > In what sense is this the case, and where can I read more about the
> > differences, as well as how to improve errors of contracts?
>
> contract-out gives better error messages than define/contract in the
> sense that it has better blame
>
> A define/contract needs to immediately decide who could be blamed for
> future errors --- because the new definition can be used right away.
>
> A contract-out can wait until another module requires the definition
> --- and tailor its blame errors to different clients.
>

My understanding is that contract-out only provides protection against
inappropriate calls from clients *outside* the module, whereas
define/contract enforces the contract against everyone, including things
inside the module.  Do I have that right?  If so, I feel much more
comfortable using the latter even if its error messages are not quite as
good.

On a related topic, I don't understand the concept of positive and negative
blame.  Can someone fill me in?


> Here's an example to play with. Submod A provides two functions: f0 is
> made with define/contract and f1 with contract-out.
>
> ```
>   #lang racket
>
>   (module A racket
> (define/contract (f0 x)
>   (-> natural? natural?)
>   x)
>
> (define (f1 x)
>   x)
>
> (provide f0)
> (provide (contract-out [f1 (-> natural? natural?)])))
>
>   (module B racket
> (require (submod ".." A))
> (f0 'hello)
> #;(f1 'hello))
>
>   (require 'B)
> ```
>
> If B makes a mistake with f0, the error blames submod A.
> But if B makes a mistake with f1, the error blames B.
>
>
> The contract library makes these blame errors internally. I don't
> think there's any way to customize short of using `contract` directly.
>
> > Is it related to this part of the documentation of `contract-out`
> > (
> https://docs.racket-lang.org/reference/attaching-contracts-to-values.html#%28form._%28%28lib._racket%2Fcontract%2Fbase..rkt%29._contract-out%29%29
> )
> > - which I admittedly don't understand:
> >
> > "The implementation of contract-out
> > <
> https://docs.racket-lang.org/reference/attaching-contracts-to-values.html#%28form._%28%28lib._racket%2Fcontract%2Fbase..rkt%29._contract-out%29%29
> >
> > uses syntax-property
> > <
> https://docs.racket-lang.org/reference/stxprops.html#%28def._%28%28quote._~23~25kernel%29._syntax-property%29%29
> >
> > to attach properties to the code it generates that records the syntax of
> > the contracts in the fully expanded program. Specifically, the symbol '
> > provide/contract-original-contract is bound to vectors of two elements,
> the
> > exported identifier and a syntax object for the expression that produces
> > the contract controlling the export."
>
> I was only thinking of the "blaming: " part of error messages.
>
> Both define/contract and contract-out can print the whole contract; I
> don't think this syntax-property gives contract-out any advantage
>
> (Sadly, the whole contract is sometimes too big to help me find a problem.)
>
> --
> 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.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/CAFUu9R5BMG5ZFVrddrJ-6uceV%2B3936ZudE-8ESObycw9B%2BRjcg%40mail.gmail.com
> .
>

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAE8gKof2M%2BHuCf%2B2hfTKbVxCxGEb1Vtx%2BaXehYNZXhttpgMNPA%40mail.gmail.com.

Re: [racket-users] Gradual Typed Racket?

2020-04-17 Thread Ben Greenman 
Hi Marc,


>> For contracts, though, (provide (contract-out ...)) gives better error
>> messages than define/contract.
>>
>
> In what sense is this the case, and where can I read more about the
> differences, as well as how to improve errors of contracts?

contract-out gives better error messages than define/contract in the
sense that it has better blame

A define/contract needs to immediately decide who could be blamed for
future errors --- because the new definition can be used right away.

A contract-out can wait until another module requires the definition
--- and tailor its blame errors to different clients.

Here's an example to play with. Submod A provides two functions: f0 is
made with define/contract and f1 with contract-out.

```
  #lang racket

  (module A racket
(define/contract (f0 x)
  (-> natural? natural?)
  x)

(define (f1 x)
  x)

(provide f0)
(provide (contract-out [f1 (-> natural? natural?)])))

  (module B racket
(require (submod ".." A))
(f0 'hello)
#;(f1 'hello))

  (require 'B)
```

If B makes a mistake with f0, the error blames submod A.
But if B makes a mistake with f1, the error blames B.


The contract library makes these blame errors internally. I don't
think there's any way to customize short of using `contract` directly.

> Is it related to this part of the documentation of `contract-out`
> (https://docs.racket-lang.org/reference/attaching-contracts-to-values.html#%28form._%28%28lib._racket%2Fcontract%2Fbase..rkt%29._contract-out%29%29)
> - which I admittedly don't understand:
>
> "The implementation of contract-out
> 
> uses syntax-property
> 
> to attach properties to the code it generates that records the syntax of
> the contracts in the fully expanded program. Specifically, the symbol '
> provide/contract-original-contract is bound to vectors of two elements, the
> exported identifier and a syntax object for the expression that produces
> the contract controlling the export."

I was only thinking of the "blaming: " part of error messages.

Both define/contract and contract-out can print the whole contract; I
don't think this syntax-property gives contract-out any advantage

(Sadly, the whole contract is sometimes too big to help me find a problem.)

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAFUu9R5BMG5ZFVrddrJ-6uceV%2B3936ZudE-8ESObycw9B%2BRjcg%40mail.gmail.com.

Re: [racket-users] Gradual Typed Racket?

2020-04-17 Thread Marc Kaufmann 
Hi Ben,

you wrote (snip):

For contracts, though, (provide (contract-out ...)) gives better error 
> messages than define/contract. 
>

In what sense is this the case, and where can I read more about the 
differences, as well as how to improve errors of contracts? Is it related 
to this part of the documentation of `contract-out` 
(https://docs.racket-lang.org/reference/attaching-contracts-to-values.html#%28form._%28%28lib._racket%2Fcontract%2Fbase..rkt%29._contract-out%29%29)
 
- which I admittedly don't understand:

"The implementation of contract-out 

 
uses syntax-property 

 
to attach properties to the code it generates that records the syntax of 
the contracts in the fully expanded program. Specifically, the symbol '
provide/contract-original-contract is bound to vectors of two elements, the 
exported identifier and a syntax object for the expression that produces 
the contract controlling the export."

Cheers,
Marc

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/a046c971-8207-4486-bfb3-723a5d7d0446%40googlegroups.com.

Re: [racket-users] Gradual Typed Racket?

2020-03-24 Thread unlimitedscolobb 

On Monday, March 23, 2020 at 9:59:22 PM UTC+1, Hendrik Boom wrote:
>
> On Mon, Mar 23, 2020 at 12:16:45PM -0400, Ben Greenman wrote: 
>
> > 
> > Not sure about best practices, but I definitely prefer keeping typed 
> > and untyped code in separate modules. 
>
> It can be veru useful to be able to mix them while in transition from one 
> to the other. 
>
> -- hendrik 
>

Absolutely!

In my case I am writing code from scratch for my research (theoretical 
computer science), but I end up wanting to write some stuff which Typed 
Racket cannot type (converting to a polymorphic type variable, for 
example), or even stuff which is difficult to type without writing long 
dependent types.  For these cases, I'd prefer to just drop the types 
"temporarily", which the different modules approach should probably allow 
me to do.

-
Sergiu

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/9bce12f3-fbba-4dec-b849-235ef573602c%40googlegroups.com.

Re: [racket-users] Gradual Typed Racket?

2020-03-23 Thread Hendrik Boom 
On Mon, Mar 23, 2020 at 12:16:45PM -0400, Ben Greenman wrote:

> 
> Not sure about best practices, but I definitely prefer keeping typed
> and untyped code in separate modules.

It can be veru useful to be able to mix them while in transition from one to 
the other.

-- hendrik

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/20200323205915.v6tj5zkzm5qmuyvu%40topoi.pooq.com.

Re: [racket-users] Gradual Typed Racket?

2020-03-23 Thread unlimitedscolobb 
Hi Ben,

Thank you for your answer!

I'll give (sub)modules a try.  The examples from the plot library are very 
helpful, I'll peruse them attentively.

I didn't realise that (provide (contract-out)) gave better error messages 
than define/contract.  I'm glad to have chosen to use (provide 
(contract-out)) in my code.

-
Sergiu


On Monday, March 23, 2020 at 5:16:52 PM UTC+1, Ben Greenman wrote:
>
> On 3/21/20, unlimitedscolobb > wrote: 
> > Hello, 
> > 
> > I come to Racket from Haskell and so far I am quite happy, as I feel 
> freer 
> > to do some weird stuff from time to time, and I am absolutely in love 
> with 
> > the Lisp-parens syntax. 
> > 
> > As a former Haskeller, one of the first things I tried was Typed Racket. 
> > It worked like a charm for small examples, but started getting in my way 
> > too much as soon as I got to some more advanced stuff (e.g. polymorphic 
> > functions, generics, eval, even apply).  My immediate reaction was 
> ditching 
> > types for contracts, which are rather fine and allow me to use a 
> familiar 
> > language, but I am somewhat worried about the performance penalties 
> > defining everything via define/contract may incur.  Also, it seems weird 
> to 
> > set up runtime contract checks where a simple type annotation would do. 
> > I have no problem with Typed Racket not being able to type every single 
> one 
> > of my functions (after all, I came to Racket to be able to do weird 
> stuff), 
> > but so far I couldn't figure out what would be the best way to mix typed 
> > into two separate files. 
> > 
> > What is the standard practice for mixing typed and untyped code within a 
> > single module?  Submodules?  Typed regions within untyped code?  Maybe 
> > there is an example somewhere I can have a look at? 
>
> Yep, submodules and typed regions are the two ways to do this. 
>
> The plot library uses typed submodules in untyped code in a few small 
> places: 
>
>
> https://github.com/racket/plot/blob/master/plot-lib/plot/private/common/contract.rkt
>  
>
> https://github.com/racket/plot/blob/master/plot-lib/plot/private/common/parameter-groups.rkt
>  
>
> I've done a similar thing to make typed parameters in untyped code. 
>
> Not sure about best practices, but I definitely prefer keeping typed 
> and untyped code in separate modules. 
>
> For contracts, though, (provide (contract-out ...)) gives better error 
> messages than define/contract. 
>

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/1aa90aad-c951-43a1-be7e-24df02ec5c67%40googlegroups.com.

Re: [racket-users] Gradual Typed Racket?

2020-03-23 Thread Ben Greenman 
On 3/21/20, unlimitedscolobb  wrote:
> Hello,
>
> I come to Racket from Haskell and so far I am quite happy, as I feel freer
> to do some weird stuff from time to time, and I am absolutely in love with
> the Lisp-parens syntax.
>
> As a former Haskeller, one of the first things I tried was Typed Racket.
> It worked like a charm for small examples, but started getting in my way
> too much as soon as I got to some more advanced stuff (e.g. polymorphic
> functions, generics, eval, even apply).  My immediate reaction was ditching
> types for contracts, which are rather fine and allow me to use a familiar
> language, but I am somewhat worried about the performance penalties
> defining everything via define/contract may incur.  Also, it seems weird to
> set up runtime contract checks where a simple type annotation would do.
> I have no problem with Typed Racket not being able to type every single one
> of my functions (after all, I came to Racket to be able to do weird stuff),
> but so far I couldn't figure out what would be the best way to mix typed
> into two separate files.
>
> What is the standard practice for mixing typed and untyped code within a
> single module?  Submodules?  Typed regions within untyped code?  Maybe
> there is an example somewhere I can have a look at?

Yep, submodules and typed regions are the two ways to do this.

The plot library uses typed submodules in untyped code in a few small places:

https://github.com/racket/plot/blob/master/plot-lib/plot/private/common/contract.rkt
https://github.com/racket/plot/blob/master/plot-lib/plot/private/common/parameter-groups.rkt

I've done a similar thing to make typed parameters in untyped code.

Not sure about best practices, but I definitely prefer keeping typed
and untyped code in separate modules.

For contracts, though, (provide (contract-out ...)) gives better error
messages than define/contract.

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAFUu9R6NyvCz2TWL4%3DBBQ0edff18LGTQcUytkXngESvrDQYx_g%40mail.gmail.com.

[racket-users] Gradual Typed Racket?

2020-03-21 Thread unlimitedscolobb 
Hello,

I come to Racket from Haskell and so far I am quite happy, as I feel freer 
to do some weird stuff from time to time, and I am absolutely in love with 
the Lisp-parens syntax.

As a former Haskeller, one of the first things I tried was Typed Racket.  
It worked like a charm for small examples, but started getting in my way 
too much as soon as I got to some more advanced stuff (e.g. polymorphic 
functions, generics, eval, even apply).  My immediate reaction was ditching 
types for contracts, which are rather fine and allow me to use a familiar 
language, but I am somewhat worried about the performance penalties 
defining everything via define/contract may incur.  Also, it seems weird to 
set up runtime contract checks where a simple type annotation would do.

I have no problem with Typed Racket not being able to type every single one 
of my functions (after all, I came to Racket to be able to do weird stuff), 
but so far I couldn't figure out what would be the best way to mix typed 
and untyped code inside a single module, ideally without having to split it 
into two separate files.

What is the standard practice for mixing typed and untyped code within a 
single module?  Submodules?  Typed regions within untyped code?  Maybe 
there is an example somewhere I can have a look at?

-
Sergiu

-- 
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.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/2b1c49ad-2076-47f7-8589-d20eff9feca1%40googlegroups.com.