for/list vs map in Typed Racket

[Daniel Prager]

The following program works in Typed Racket, but if you comment out the for/list in (encode ...) and uncomment the seemingly equivalent map it fails to type check.

Why the discrepancy and how do the experienced Typed Racketeers diagnose and fix these sorts of issues?

Thanks

Dan

P.S. These are taken from Nintey-nine Lisp Problems:

http://www.ic.unicamp.br/~meidanis/courses/mc336/2006s2/funcional/L-99_Ninety-Nine_Lisp_Problems.html

#lang typed/racket

(require typed/test-engine/racket-tests)

;P09 (**) Pack consecutive duplicates of list elements into sublists.

(: pack : (All (a) (Listof a) -> (Listof (Listof a))))

(define (pack xs)

  (cond [(null? xs) null]

        [(null? (rest xs)) (list xs)]

        [else (let ([packed (pack (rest xs))]

                    [head (first xs)])

                (if (equal? (first xs) (second xs))

                    (cons (cons head (first packed))

                          (rest packed))

                    (cons (list head) packed)))]))

                          

(check-expect (pack '(a a a a b c c a a d e e e e))

              '((a a a a) (b) (c c) (a a) (d) (e e e e)))

;P10 (*) Run-length encoding of a list.

(: encode : (All (a) (Listof a) ->

                 (Listof (List Nonnegative-Integer a))))

(define (encode xs)

  #;(map (λ (ys) (list (length ys) (first ys))) (pack xs))

  (for/list ([ys (pack xs)])

    (list (length ys) (first ys))))

(check-expect (pack '(a a a a b c c a a d e e e e))

              '((a a a a) (b) (c c) (a a) (d) (e e e e)))

(test)

[Sam Tobin-Hochstadt]

What's happening here is that Typed Racket can't infer what the type
of `ys` is in the lambda that's an argument to `map`, since you didn't
provide an annotation. In the `for/list`, the call to `(pack xs)` is
right there, so inference works.

To make the use of `map` work, you just annotate `ys`: (λ ([ys :
(Listof a)]) (list (length ys) (first ys)))

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...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Daniel Prager]

Thanks Sam

I still get a type-checking error with

(: encode : (All (a) (Listof a) -> (Listof (List Nonnegative-Integer a))))

(define (encode xs)

  (map (λ ([ys : (Listof a)])

         (list (length ys) (first ys))

       (pack xs)))) 

which I think is what you suggested. Adding a return type to the λ as well yields more type errors.

Dan

[Matthias Felleisen]

1. You had a } mistake. 

2. You are using a polymorphic map and TR needs an additional annotation to figure this out: 

(: encode : (All (a) (Listof a) -> (Listof (List Nonnegative-Integer a))))

(define (encode xs)

  ({inst map (List Nonnegative-Integer a) (Listof a)}

   (λ ([ys : (Listof a)])

     (list (length ys) (first ys)))

   (pack xs)))

3. I provided a pack of type (: pack (All (a) (Listof a) -> (Listof (Listof a))))  

4. When you run this now, (first ys) may raise a run-time exception (just like in ML). 

[Robby Findler]

So: yet one more reason to prefer for/list over map? :)

Robby

[Matthias Felleisen]

Try typing that one :-)

[Sam Tobin-Hochstadt]

That program works fine for me. The full code that I ran is here:
https://gist.github.com/samth/0992fff495cbff20e4aed96522c69332

Sam

[Daniel Prager]

Thank-you Matthias

On Wed, May 25, 2016 at 10:46 PM, Matthias Felleisen <matt...@ccs.neu.edu> wrote:

1. You had a } mistake.

I see it now.

By putting an extra ) at the end of the λ I committed an arity error.

I could have seen this in DrRacket if I formatted as you did, with the separate arguments to map on distinct lines: indentation would have given the hint.

In regular Racket this kind of error passes compile, but there's a nice arity error at run-time.

Typed Racket gives a confusing error at type-check time instead.

How difficult would it be to have compile time arity checks be prior to type checking in TR? The idea being to give simpler error messages where possible.

3. I provided a pack of type (: pack (All (a) (Listof a) -> (Listof (Listof a))))  

4. When you run this now, (first ys) may raise a run-time exception (just like in ML). 

If pack is "correctly" implemented this should not be possible, but I take it this is not expressible using Typed Racket types.

You'd want something like:

(: pack (All (a) (Listof a) -> (Listof ("NonemptyListof" a))))

Shades of dependent types?

Dan  

[Sam Tobin-Hochstadt]

You can write `(NonemptyListof a)` as

(define-type (NonemptyListof a) (Cons a (Listof a)))

Sam



On Wed, May 25, 2016 at 5:08 PM, Daniel Prager
<daniel....@gmail.com> wrote:
> Thank-you Matthias

>
> On Wed, May 25, 2016 at 10:46 PM, Matthias Felleisen <matt...@ccs.neu.edu>
> wrote:
>>
>>

>> 1. You had a } mistake.
>
>

> I see it now.
>
> By putting an extra ) at the end of the λ I committed an arity error.
>
> I could have seen this in DrRacket if I formatted as you did, with the
> separate arguments to map on distinct lines: indentation would have given
> the hint.
>
> In regular Racket this kind of error passes compile, but there's a nice
> arity error at run-time.
>
> Typed Racket gives a confusing error at type-check time instead.
>
> How difficult would it be to have compile time arity checks be prior to type
> checking in TR? The idea being to give simpler error messages where
> possible.
>
>

>> 3. I provided a pack of type (: pack (All (a) (Listof a) -> (Listof
>> (Listof a))))
>
>
>>
>> 4. When you run this now, (first ys) may raise a run-time exception (just
>> like in ML).
>
>

[Daniel Prager]

On Thu, May 26, 2016 at 7:13 AM, Sam Tobin-Hochstadt <sa...@cs.indiana.edu> wrote:

You can write `(NonemptyListof a)` as

    (define-type (NonemptyListof a) (Cons a (Listof a)))

Sam

Nice: Cons -> Pairof, though.

Dan