[racket] typing a function

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Thu Nov 22 11:47:12 EST 2012

On Nov 21, 2012, at 11:34 AM, Pierpaolo Bernardi wrote:

> #lang typed/racket
> 
> (define-type sex (U -1 0 1))
> 
> (struct: sexomino
>  ((n : sex)
>   (e : sex)
>   (s : sex)
>   (o : sex)))
> 
> (: sexomini (Listof sexomino))
> (define sexomini
>  (let ()
>    (define n 0)
>    (define f -1)
>    (define m 1)
>    (define s sexomino)
>    (list (s n m n n) (s f f n n))))


I believe nobody responded. On occasion the type checker needs help narrowing down a type, as in your example. Specifically, the type checker on occasion guesses (fancy word is: "locally infers") a type and to make programming convenient, it guesses a little larger than good for things like your example. The easy fix is

#lang typed/racket

(define-type sex (U -1 0 1))

(struct: sexomino
         ((n : sex)
          (e : sex)
          (s : sex)
          (o : sex)))

(: sexomini (Listof sexomino))
(define sexomini
  (let ()
    (define n 0)
    (: f sex)
    (define f -1)
    (define m 1)
    (define s sexomino)
    (list (s n m n n) (s f f n n))))

This is a compromise to accommodate code from an untyped basis mostly as is and helping programmers find even narrower types when they wish to make sharp invariants explicit. 

Think of TR as a wide-spectrum typed programming experience 

-- Matthias



-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4373 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20121122/c3c61f07/attachment-0001.p7s>

Posted on the users mailing list.