[plt-scheme] Typed-Scheme and car

On Sun, Apr 5, 2009 at 6:30 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
> On Sun, Apr 5, 2009 at 6:18 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>>
>> Would this
>>
>>> #lang typed-scheme
>>>
>>> (define x (list (cons 'one 1) (cons 'two 2) (cons 'three 3)))
>>>
>>> (define y ({inst map Symbol (Pair Symbol Integer)} car x))
>>
>> make you happier? Local inference can't infer at which type map is used
>> here. That's why you need to declare it.
>>
>
> If no inference is possible that's definitely better. Seems I am still
> learning my way around typed-scheme. :)
>

Something else I would say is that it's not really clear why you type
map with Symbol and (Pair Symbol Integer), since map receives in this
case a function (Pair Symbol Integer) returning a Symbol and a (Listof
 (Pair Symbol Integer)) itself returns a (Listof Symbol). So, having
{inst map Symbol (Pair Symbol Integer)} is quite unclear. I understand
that we are assigning specific types to the polymorphic types of the
type definition for map, but the problem is that the user needs to
know how the type of a specific function is written (order of types
and polymorphic variables used) and none of this seems written
anywhere. For example, even if know that map needs to be explicitly
typed in this case, why {inst map Symbol (Pair Symbol Integer)} and
not {inst map (Pair Symbol Integer) Symbol} ?

Cheers,

Paulo Matos

> Thanks,
>
> Paulo Matos
>
>> -- Matthias
>>
>>
>>
>> On Apr 5, 2009, at 1:57 PM, Paulo J. Matos wrote:
>>
>>> Hi all,
>>>
>>> Just trying this example I got two unexpected error:
>>> #lang typed-scheme
>>>
>>> (: x (Listof (Pair Symbol Integer)))
>>> (define x '((one . 1) (two . 2) (three . 3)))
>>>
>>> (: y (Listof Symbol))
>>> (define y (map car x))
>>>
>>> . typecheck: Expected (Listof (Pair Symbol Integer)), but got (List
>>> Any Any Any) in: (quote ((one . 1) (two . 2) (three . 3)))
>>> . typecheck: Polymorphic function map could not be applied to arguments:
>>> Domain: (a b ... b -> c) (Listof a) (Listof b) ... b
>>> Arguments: (All (a b) (case-lambda ((Pair a b) -> a) ((Listof a) ->
>>> a))) (Listof (Pair Symbol Integer))
>>> Result type: (Listof c)
>>> Expected result: (Listof Symbol)
>>>  in: (map car x)
>>>
>>> if I replace x define with:
>>> (define x (list (cons 'one 1) (cons 'two 2) (cons 'three 3)))
>>>
>>> the first error disappears but the second remains. The second error
>>> goes away with:
>>> (define y (map (lambda: ((p : (Pair Symbol Integer))) (car p)) x))
>>>
>>> But this is MUCH more annoying to write and the program gets much more
>>> verbose and I have to say that after rewriting a couple of 'big'
>>> modules in typed-scheme, the scheme simplicity and elegance starts to
>>> fade. Making typed-scheme support things such as a (map car x) is for
>>> me a big requirement. Currently my code is full of lambda: in maps,
>>> filters, etc for no good reason. I hope that there is work to improve
>>> this in the future. I guess it is possible to make the type inference
>>> mechanism to detect this.
>>>
>>> Still, cheers and kudos to Sam and other for the current state of
>>> typed-scheme. It is a very nice language to program in even though its
>>> current state still has some quirks.
>>>
>>>
>>> --
>>> Paulo Jorge Matos - pocmatos at gmail.com
>>> Webpage: http://www.personal.soton.ac.uk/pocm
>>> _________________________________________________
>>>  For list-related administrative tasks:
>>>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>>
>>
>
>
>
> --
> Paulo Jorge Matos - pocmatos at gmail.com
> Webpage: http://www.personal.soton.ac.uk/pocm
>



-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm