[racket] Defining a typed language

From: Konrad Hinsen (konrad.hinsen at fastmail.net)
Date: Thu Oct 16 11:41:21 EDT 2014

Konrad Hinsen writes:

 > After a closer look at the language definition mechanism, I came to the
 > conclusion that the language here is actually "s-exp", with my module
 > merely providing the initial bindings.
 > 
 > So what I seem to need is typed/s-exp, but that doesn't exist. How
 > would I go about writing this myself? The implementation of s-exp
 > is simple enough, but I don't see anything in there that says if it's
 > a typed or an untyped language.

I changed my approach to defining a "full" language, not just a
variant of s-exp. After exploring how Typed Racket itself is set up, I
defined a language "test-lang" consisting of the following parts:

-- test-lang/main.rkt ----------------------------
#lang typed-racket/minimal

(require typed/racket
         test-lang/more)

(provide (all-from-out typed/racket)
         (all-from-out test-lang/more))
--------------------------------------------------

-- test-lang/more.rkt ----------------------------
#lang typed/racket

(provide bar)

(: bar (-> Integer Integer))
(define (bar x)
  (* 2 x))
--------------------------------------------------

-- test-lang/lang/reader.rkt ---------------------
#lang s-exp syntax/module-reader

test-lang/main

#:read r:read
#:read-syntax r:read-syntax

(require (prefix-in r: typed-racket/typed-reader))
--------------------------------------------------

With those files in place (in a collection), I try to run

-- test.rkt --------------------------------------
#lang test-lang

(: x Integer)
(define x 42)
(print x)

(print (bar x))
--------------------------------------------------

This results in an error message:

; test-lang/more.rkt:4:9: Type Checker: missing type for identifier;
;  consider using `require/typed' to import it
;   identifier: bar
;   from module: test-lang/more
;   in: bar

But 'bar' in test-lang/more has a type annotation, and if I 
do (require test-lang/more) explicitly, everything works fine.
So where does the type annotation for bar disappear?

Konrad

Posted on the users mailing list.