Next: , Previous: , Up: 2016   [Contents][Index]


On type propagation and other stuff

Posted on May 2, 2016

More work in the ‘typed-languagebranch of Vicare, for both the expander and the built–in types infrastructure. (Lately I always open with the same paragraph, cut and pasted; that is what it is.)

Everything I discuss here is relative to code in the head of the ‘typed-language’ branch.

Type propagation across built–in syntaxes

I anticipated in a previous post that I would reconsider RHS type propagation, and I did. I have implemented type propagation for some syntaxes. It works like this:

(type-of 1)
⇒ #[signature (<positive-fixnum>)]

(type-of (let ((A 1))
           (let* ((B A)
                  (C B))
             (letrec ((D C))
               (letrec* ((E D)
                         (F E))
                 (define (G)
                   F)
                 (define H
                   (G))
                 ((lambda () H)))))))
⇒ #[signature (<positive-fixnum>)]

the initial type of 1 is propagated through the syntactic bindings A, B, C, D, E, F, G, H and the last thunk application.

When a lexical variable is mutated: its type must be compatible with the hard–coded type annotation or the inferred type annotation. This is fine:

(let ((A "ciao"))
  (set! A "hello")
  A)

but this will fail:

(let ((A 1))
  (set! A -1)
  A)

because initially A is annotated with <positive-fixnum>, then set! attempts to mutate it with a value that is of type <negative-fixnum>. In these cases we have to explicitly include the type annotation in the source:

(let (({A <fixnum>} 1))
  (set! A -1)
  A)

where <fixnum> is an ancestor of both <positive-fixnum> and <negative-fixnum>.

type-of as type annotation

There is a new type annotation syntax: type-of. When used in expression context: type-of expands to a type signature object representing the type of the expression. When used in type annotation context: it describes the type of the given expression.

There are limitations: the expression must return a single value of known type; the expression is expanded and not evaluated, this means the side effects of the expansion are performed (use with care!).

(type-annotation-syntax (type-of 123))
⇒ <positive-fixnum>

(type-annotation-syntax (type-of (void)))
⇒ <void>

(let ((fun (lambda () 123)))
  (type-annotation-syntax (type-of (fun))))
⇒ <positive-fixnum>

(type-annotation-syntax (or (type-of 1)
                            (type-of "ciao")
                            (type-of 'hey)))
⇒ (or <positive-fixnum> <string> (enumeration hey))

This is actually used by Vicare to implement type propagation for a common idiom when using case. Without special handling:

(type-of
  (case (read)
    ((1 "2" 'ciao) => (lambda (x) x))
    (else #f)))
⇒ #[signature (<top>)]

because the expansion of case has no way to infer that when read returns 1 or "2" or ciao the closure object returns that value itself. But with special handling, the closure object is transformed to:

(lambda ({x (or (type-of 1)
                (type-of "2")
                (type-of 'ciao))})
  x)

and so:

(type-of
  (case (read)
    ((1 "2" 'ciao) => (lambda (x) x))
    (else #f)))
⇒ #[signature ((or <positive-fixnum> <string> (enumeration ciao) <false>))]

Handling of void

There is an experimental change that may cause troubles: expressions of type <void> are forbidden as operands in function applications and logic predicates. For example:

(display (vector-set! (vector 1) 0 2))

should raise an error because vector-set! returns the void value. The type <void> has no parent (it is not a sub–type of <top>) and it should be like not–a–number for numeric computations. It is not yet clear if this will cause problems. Here are some consequences:

Chez Scheme has been open sourced

These are my opinions. Every Scheme implementation maintainer feels the pressure of Racket’s growth… so you have to do something otherwise Racket will eat your lunch. They had to wait for a while before open–sourcing it, because a Chez Scheme license was really costly: you do not want to make your customers angry by selling them a costly product and then open–sourcing it after five minutes.

I wonder if open–sourcing it five years ago would have made a difference for R6RS. Ah… forget it!

Compiling Vicare’s boot image takes a lot… you know?

I started keeping a deck of cards near the laptop; I like le piacentine. So, while compiling, I play a solitaire with true cards. I like one called the cross: I cannot explain it here, but it is simple, things happen, and takes small room on the desk. Even randomising the deck is relaxing in itself.


Next: , Previous: , Up: 2016   [Contents][Index]