Пользовательский набор ha sh в набранной ракетке приводит к нарушению договора с объектами синтаксиса - PullRequest
Новая
       5

Пользовательский набор ha sh в набранной ракетке приводит к нарушению договора с объектами синтаксиса

2 голосов
/ 25 марта 2020

У меня есть пользовательский набор , и я хочу использовать его в набранной ракетке. Мне требуется, используя require/typed с инструкцией #:opaque custom-set?. Это работает, за исключением того, что код не выполняется во время выполнения, когда я вызываю custom-set? с синтаксическим объектом.

У меня есть что-то вроде следующего: 

#lang typed/racket/base

(module UNTYPED racket/base
  (require racket/set)
  (provide custom-set?
           make-immutable-custom-set)

  (define-custom-set-types custom-set
    #:elem? identifier?
    (λ (id1 id2) (eq? (syntax-e id1) (syntax-e id2)))))

(require/typed 'UNTYPED
  [#:opaque MySet custom-set?]
  [make-immutable-custom-set ((Listof Identifier) -> MySet)])

(custom-set? (make-immutable-custom-set (list #'foo #'bar)))  ;; #t
(custom-set? '())  ;; #f

Какой тип проверяет и возвращает #t или #f, как и ожидалось.

Теперь, если я попытаюсь вызвать тот же самый предикат custom-set? с синтаксическим объектом: 

(custom-set? #'(foo bar))

Затем я получу следующее нарушение контракта вместо #f: 

custom-set?: broke its own contract
  Attempted to use a higher-order value passed as `Any` in untyped code: #<syntax:stdin:: a>
  in: the 1st argument of
      a part of the or/c of
      (or/c
       struct-predicate-procedure?/c
       (-> Any boolean?))
  contract from: (interface for custom-set?)
  blaming: (interface for custom-set?)

Тот же самый вызов в модуль UNTYPED работает и возвращает #f, как и ожидалось. Не могли бы вы сказать мне, почему объект синтаксиса нарушает контракт здесь? И можно ли это исправить?

1 Ответ

2 голосов
/ 25 марта 2020

Это ошибка, вызванная тем, что контракты синтаксических объектов недостаточно хороши. В частности, syntax/c контракт работает с плоскими контрактами, в то время как Typed Racket хочет работать с контрактами-компаньонами, когда задействован тип Any.

Any, который здесь используется, является неявным введением Any на #:opaque требуется предикат custom-set?. Он появляется во входных данных, защищая значения, которые начинаются в типизированном коде и заканчиваются нетипизированным кодом. Поскольку нетипизированный код может пытаться связываться с типизированным значением высшего порядка, он должен быть заключен в контракт с компаньоном any-wrap/c (внутренний для Typed Racket).

any-wrap/c предназначен для защиты потенциально более высокого уровня. значения порядка и значения контейнера, которые могут содержать значения более высокого порядка. Если какая-то часть была изменяемой или если какая-то часть имела функцию в ней, нетипизированному коду нельзя разрешать изменять эти данные или вызывать эту функцию.

Синтаксические объекты являются контейнерами. Они могут содержать произвольные значения в «синтаксис-е» и свойства синтаксиса. В идеале контракт Typed Racket any-wrap/c должен заключать объекты синтаксиса в контракты-компаньоны, защищающие эти места. К сожалению, контракт syntax/c в системе контрактов недостаточно хорош для этого. Из-за этого синтаксиса объекты считаются «небезопасными» контейнерами, и если any-wrap/c не может их безопасно обернуть, это должно вызвать ошибку контракта.

Единственный способ, которым я могу видеть, что это может быть исправлено в будущем, это улучшив syntax/c для работы с контрактами-компаньонами. После этого any-wrap/c может считать синтаксические объекты безопасными контейнерами, как списки.

...