Gradual Typed Racket?

[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

[Ben Greenman]

On 3/21/20, unlimitedscolobb <unlimite...@gmail.com> 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.

[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

[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

[unlimitedscolobb]

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

[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

[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

> <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.)

[David Storrs]

On Fri, Apr 17, 2020 at 9:45 AM Ben Greenman <benjamin...@gmail.com> 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?

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

[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.

 

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

[Ben Greenman]

On 4/17/20, Sorawee Porncharoenwase <sorawe...@gmail.com> 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.

[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.

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