Re: [racket-users] Typed racket and continuations

[Andrew Kent]

@Jerzy here's (perhaps an unneeded) clarification just in case it helps:
Matthias said initially in a set theoretic type system continuations could
be considered as having the empty set as their return _type_ (not value) --
or in other words, their return type would be the empty type, or bottom
(which I believe is the "dramatic" something you had suggested). In Typed
Racket (U) is bottom (also written 'Nothing' in Typed Racket)).

On Tue, Aug 30, 2016 at 9:10 AM Matthias Felleisen 
wrote:

>
> > On Aug 30, 2016, at 3:22 AM, Jerzy Karczmarczuk <
> jerzy.karczmarc...@unicaen.fr> wrote:
> >
> > Could anybody justify this convention?
>
>
> Here the empty set represents the set of all possible result values.
> That’s a meta-set or a set about things in the language.
>
> > An empty set is a legitimate piece of data.
>
> If you wanted a function to return the empty set as a piece of data, you
> would have to choose a set representation.
>
> In principle, you ought to be able to construct a singleton type that
> expresses that a function will return the empty set.
>
> — Matthias
>
> --
> 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 and continuations

[Matthias Felleisen]

> On Aug 30, 2016, at 3:22 AM, Jerzy Karczmarczuk 
>  wrote:
> 
> Could anybody justify this convention?


Here the empty set represents the set of all possible result values. That’s a 
meta-set or a set about things in the language. 

> An empty set is a legitimate piece of data. 

If you wanted a function to return the empty set as a piece of data, you would 
have to choose a set representation. 

In principle, you ought to be able to construct a singleton type that expresses 
that a function will return the empty set. 

— Matthias

-- 
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 and continuations

[Robby Findler]

The reason the first one doesn't work is that the type checker has
figured out that the variable is mutable and HASN"T figured out that
there are no other threads around that could mutate it. In the second
case, it knows there are no other threads around to mutate it because
even if there were other threads, there is no set!, so it can't be
mutated.

Robby


On Tue, Aug 30, 2016 at 7:44 AM, Alex Knauth  wrote:
>
> On Aug 30, 2016, at 2:08 AM, Sourav Datta  wrote:
>
> I tried this approach with Racket 6.5 and still get the type checker error
> when trying to call the continuation after it has been set.
>
> #lang typed/racket
>
> (define-type EmptySet (U))
>
> (: d-or-s (U False (-> Number EmptySet)))
> (define d-or-s #f)
>
> (: double-or-same (-> Number Number))
> (define (double-or-same x)
> (call/cc (lambda ({c : (-> Number EmptySet)})
>(set! d-or-s c)
>(+ x x
>
> (double-or-same 10)
>
> - : Number
> 20
>
> (d-or-s 1)
>
> . Type Checker: Cannot apply expression of type (U False (-> Number
> Nothing)), since it is not a function type in: (d-or-s 1)
>
> d-or-s
>
> - : (U False (-> Number Nothing))
> #
>
> Not sure why the type checker is complaining that d-or-s is not a function
> type.
>
>
> You're right, the (U False (-> Number EmptySet)) can't be applied directly.
> The reason is that it might be a function type, but it also might be false.
> Applying false as a function would be a type error, so applying something
> that might be false is also a type error.
>
> The way around this should be occurrence typing. The first thing to try is
> an if statement like this:
>
>> (if d-or-s
>   (d-or-s 1)
>   "it wasn't a function")
> . Type Checker: Cannot apply expression of type (U False (-> Number
> Nothing)), since it is not a function type in: (d-or-s 1)
>
> However, it raises the same type error as before. The reason is that
> `d-or-s` being mutable messes it up. The way to get around that is to make a
> new local variable to use in the if statement. Since `f` isn't mutable,
> occurrence typing can work on it, and you can call `f` within the
> then-branch.
>
>> (let ([f d-or-s])
> (if f
> (f 1)
> "it wasn't a function"))
> 1
>
> Alex Knauth
>
> --
> 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 and continuations

[Alex Knauth]

> On Aug 30, 2016, at 2:08 AM, Sourav Datta  wrote:
> 
> I tried this approach with Racket 6.5 and still get the type checker error 
> when trying to call the continuation after it has been set.
> 
> #lang typed/racket
> 
> (define-type EmptySet (U)) 
> 
> (: d-or-s (U False (-> Number EmptySet))) 
> (define d-or-s #f) 
> 
> (: double-or-same (-> Number Number)) 
> (define (double-or-same x) 
> (call/cc (lambda ({c : (-> Number EmptySet)}) 
>(set! d-or-s c) 
>(+ x x 
> 
>> (double-or-same 10)
> - : Number
> 20
>> (d-or-s 1)
> . Type Checker: Cannot apply expression of type (U False (-> Number 
> Nothing)), since it is not a function type in: (d-or-s 1)
>> d-or-s
> - : (U False (-> Number Nothing))
> #
> 
> Not sure why the type checker is complaining that d-or-s is not a function 
> type.

You're right, the (U False (-> Number EmptySet)) can't be applied directly. The 
reason is that it might be a function type, but it also might be false. 
Applying false as a function would be a type error, so applying something that 
might be false is also a type error.

The way around this should be occurrence typing. The first thing to try is an 
if statement like this:

> (if d-or-s
  (d-or-s 1)
  "it wasn't a function")
. Type Checker: Cannot apply expression of type (U False (-> Number Nothing)), 
since it is not a function type in: (d-or-s 1)

However, it raises the same type error as before. The reason is that `d-or-s` 
being mutable messes it up. The way to get around that is to make a new local 
variable to use in the if statement. Since `f` isn't mutable, occurrence typing 
can work on it, and you can call `f` within the then-branch.

> (let ([f d-or-s])
(if f
(f 1)
"it wasn't a function"))
1

Alex Knauth

-- 
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 and continuations

[Jerzy Karczmarczuk]

Le 30/08/2016 à 02:26, Hendrik Boom a écrit :

On Mon, Aug 29, 2016 at 04:33:15PM -0400, Matthias Felleisen wrote:

Continuations don’t return. In a set-oriented type system this means their 
result type is the empty set:

I tried, but failed, to get this convention into Algol 68 for
functinos that don't return.

-- hendrik

Could anybody justify this convention?
An empty set is a legitimate piece of data. In the non-deterministic 
monad in Haskell the empty list means a failure, a "no answer" result, 
but a result anyway.
In my head I always saw the non-returning functions as yielding 
something more "dramatic", a bottom perhaps?...


Jerzy Karczmarczuk
/Caen, France/

--
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 and continuations

[Matthias Felleisen]

Continuations don’t return. In a set-oriented type system this means their 
result type is the empty set: 

#lang typed/racket

(define-type EmptySet (U))

(: d-or-s (U False (-> Number EmptySet)))
(define d-or-s #f)

(: double-or-same (-> Number Number))
(define (double-or-same x)
 (call/cc (lambda ({c : (-> Number EmptySet)})
(set! d-or-s c)
(+ x x


> On Aug 29, 2016, at 2:18 PM, Sourav Datta  wrote:
> 
> Hey everyone,
> 
> I am a beginner in Racket and recently learned the basic concepts of 
> continuations. I like Racket's support of multiple types of continuations as 
> opposed one type in Scheme. Recently I also started learning about typed 
> Racket. My problem is, I am not sure how I can annotate a continuation in a 
> typed racket program. For example, when trying to annotate the below code:
> 
> #lang racket
> 
> (define d-or-s #f)
> 
> (define (double-or-same x)
>  (call/cc (lambda (c)
> (set! d-or-s c)
> (+ x x
> 
> in typed racket, I can see that double-or-same function can have type 
> (Integer -> Integer). But what should be the type of the variable do-or-s? If 
> it is Any, then it cannot be called like a function after the continuation is 
> set to it. So basically my question is how can we type annotate different 
> types of continuations starting from a simple one like the above? Also a 
> pointer to the relevant section in typed racket docs would be great.
> 
> Thanks!
> 
> -- 
> 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] Typed racket and continuations

[Sourav Datta]

Hey everyone,

I am a beginner in Racket and recently learned the basic concepts of 
continuations. I like Racket's support of multiple types of continuations as 
opposed one type in Scheme. Recently I also started learning about typed 
Racket. My problem is, I am not sure how I can annotate a continuation in a 
typed racket program. For example, when trying to annotate the below code:

#lang racket

(define d-or-s #f)

(define (double-or-same x)
  (call/cc (lambda (c)
 (set! d-or-s c)
 (+ x x

in typed racket, I can see that double-or-same function can have type (Integer 
-> Integer). But what should be the type of the variable do-or-s? If it is Any, 
then it cannot be called like a function after the continuation is set to it. 
So basically my question is how can we type annotate different types of 
continuations starting from a simple one like the above? Also a pointer to the 
relevant section in typed racket docs would be great.

Thanks!

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