Как использовать with-type для использования фрагментов Typed Racket в нетипизированных модулях?

В справочнике по Typed Racket указано, что можно использовать with-type для создания "типизированных областей" в нетипизированном коде.

with-type позволяет использовать локализованные области Typed Racket в нетипизированном коде.

Однако немного неясно, как на самом деле использовать это. Очевидно, что использование такой функции должно происходить в нетипизированном модуле с использованием #lang racket или чего-то подобного. Как следует импортировать привязку with-type?

Наивная попытка состоит только в require типизированном рэкете, но это приводит к сбоям в том, как TR перезаписывает существующие синтаксические формы.

(require typed/racket)

(struct point (x y)) ; complains about missing type annotations

Попытка использовать only-in для простого требования with-type и ничего другого не работает, но тогда не существует ни одной из требуемых привязок типов (таких как Number или ->).

Кажется, что единственный способ сделать это — вручную использовать only-in для импорта только тех вещей, которые мне нужны, но это кажется трудоемким. Я мог бы и prefix-in использовать, но тогда конечно все было бы разбросано префиксами.

Есть ли рекомендуемый способ сделать это, или эта функция несколько устарела?


person Alexis King    schedule 08.03.2015    source источник


Ответы (2)


Я бы просто использовал except-in (или, возможно, rename-in), чтобы избежать нескольких идентификаторов, которые не работают как в типизированных, так и в нетипизированных программах. Как эта модификация программы Грега:

#lang racket/base

(require (except-in typed/racket struct))

(struct point (x y))

(let ([x 'hello])
  (with-type
    #:result String
    #:freevars ([x String])
    (string-append x ", world")))
person Sam Tobin-Hochstadt    schedule 10.03.2015
comment
Я приму это как канонический ответ. Я бы хотел, чтобы это было лучше, но я действительно не вижу лучшего возможного способа, не делая ничего действительно сумасшедшего. - person Alexis King; 11.03.2015

Я не знаю фундаментального ответа. Предполагается, что это было бы полезно при написании макросов, в отличие от кода, который вы бы написали напрямую?

Практическая идея: вы можете использовать local-require, чтобы ограничить "загрязнение" запроса TR. И вы можете переключиться на использование except-in, если это менее трудозатратно, чем only-in.

Например, этот пример из документации приближается, но дает странную ошибку, предположительно потому, что он использует TR quote:

#lang racket/base

(let ([x 'hello])
  (local-require typed/racket)
  (with-type
    #:result String
    #:freevars ([x String])
    (string-append x ", world")))
; /tmp/so.rkt:7:21: quote: identifier used out of context
;   in: quote

За исключением того, что с except-in выдает нужную ошибку:

(let ([x 'hello])
  (local-require (except-in typed/racket quote))
  (with-type
    #:result String
    #:freevars ([x String])
    (string-append x ", world")))
; x: broke its contract
;   promised: String
;   produced: 'hello
;   in: String
;   contract from: /tmp/so.rkt
;   blaming: /tmp/so.rkt
;    (assuming the contract is correct)
;   at: /tmp/so.rkt:14.17

Но да. Это просто игра с краями и не добраться до сути.

person Greg Hendershott    schedule 09.03.2015