[racket] Puzzled about type inference

Matthias, hello.

On 2014 Aug 5, at 14:23, Matthias Felleisen <matthias at ccs.neu.edu> wrote:

> --- 1. There was no contradiction between Sam's email (happy birthday Sam) and mine.

On the contrary, I thought it was useful to see, between three alternatives, the contrast between a minimally- and a maximally-rewritten version.

> 	add type declarations to variables and fields and function and method signatures. 

A good motto, which I shall endeavour to remember.

> Bottom line is then, TR is in an actual state and then there is the ideal that some of us have in our head where local type inference does a lot more and becomes almost as good as GLOBAL ti in terms of convenience. It is critical to keep this in mind. TR isn'f finished and it will continue to move from 'actual' to 'ideal'. 

Keep on keeping on!

In case anyone's interested, the actual code ended up looking as below.

Thanks, all, for a most illuminating thread.

Best wishes,

Norman


----

(define-type LevelN Positive-Integer)
(define-type Backup-Log (Vectorof (Maybe LevelN)))
(require/typed db
               [#:opaque Handle connection?]
               [query-value (Handle String SQLType * -> SQLType)]
               [query-rows (Handle String SQLType * -> (Listof (Vectorof SQLType)))])

[...]

(: get-latest-backups/filesystem
   (case->
    (Handle String -> Backup-Log)
    (Handle String String -> Backup-Log)))
(define (get-latest-backups/filesystem db fs [refdate #f])
  ;; I can't see any way to do this in a single SQL statement
  (let ((parent0 (query-value db
                              "select parent0 from backups where filesystem=$1 and created<$2 order by created desc limit 1"
                              fs
                              (or refdate (reftime/iso8601)))))
    (define-type VIL (Vector Positive-Integer LevelN))
    (define idx+level : (Listof VIL)
      (cast (query-rows db ; only idx=0 can have a level=0 backup
                        "select idx, level from backups where parent0=$1 and idx > 0"
                        parent0)
            (Listof VIL)))
    (define length : Positive-Integer
      (1+ (apply max (map (λ ([x : VIL]) (vector-ref x 0)) idx+level))))
    (define result : Backup-Log
      (make-vector length #f))

    (for ((q : VIL (in-list idx+level)))
      (vector-set! result (vector-ref q 0) (vector-ref q 1)))
    result))



-- 
Norman Gray  :  http://nxg.me.uk
SUPA School of Physics and Astronomy, University of Glasgow, UK