Ввод символов с полиморфными типами объединения

Question

Предположим, я хочу преобразовать следующий нетипизированный код в типизированную ракетку. Эти функции вдохновлены SICP, где они показывают, как структура данных может быть построена исключительно из функций.

(define (make-pair x y) 
    (lambda (c) 
     (cond 
      ((= c 1) x) 
      ((= c 2) y) 
      (error "error in input, should be 1 or 2")))) 

(define (first p) (p 1)) 
(define (second p) (p 2)) 

Чтобы преобразовать его прямо в типизированных ракетку, возвращаемое значение функции make-pair, кажется (: make-pair (All (A B) (-> A B (-> Number (U A B))))). И после этого тип first должен быть (: first (All (A B) (-> (-> Number (U A B)) A))). Однако при реализации функции мы не можем позвонить (p 1) прямо сейчас, потому что нам нужно что-то типа ввода, чтобы убедиться, что first возвращает только тип A. Изменение типа возврата first на (U A B) работает, но тогда нагрузка на вхождение вводится пользователю, а не в API. Таким образом, в этом случае мы можем использовать встраивание ввода внутри first (то есть, как использовать предикат для переменной типа A), чтобы мы могли безопасно вернуть только первый компонент пары?

ОБНОВЛЕНИЕ

Я попробовал подход, который отличается немного сверху и требует предикатов для A и B, которые поставляются в качестве аргументов make-pair функции. Ниже приведен код:

#lang typed/racket 


(define-type FuncPair (All (A B) (List (-> Number (U A B)) (-> A Boolean) (-> B Boolean)))) 

(: make-pair (All (A B) (-> A B (-> A Boolean) (-> B Boolean) (FuncPair A B)))) 
(define (make-pair x y x-pred y-pred) 
    (list 
     (lambda ([c : Number]) 
      (cond 
       ((= c 1) x) 
       ((= c 2) y) 
       (else (error "Wrong input!")))) 
     x-pred 
     y-pred)) 

(: first (All (A B) (-> (FuncPair A B) Any))) 
(define (first p) 
    (let ([pair-fn (car p)] 
      [fn-pred (cadr p)]) 
     (let ([f-value (pair-fn 1)]) 
      (if (fn-pred f-value) 
       f-value 
       (error "Cannot get first value in pair"))))) 

Однако это не удается в чековой (fn-pred f-value) состоянии с ошибкой expected: A given: (U A B) in: f-value

Answer 1

Из бестипового кода в начале вашего вопроса, похоже, пара A и B является функция, которая дается 1, возвращает а, и с учетом 2, отдает Б. способ выразить этот тип функции с типом case->:

#lang typed/racket 

(define-type (Pairof A B) 
    (case-> [1 -> A] [2 -> B])) 

аксессоров ч п определяется так же, как ваш оригинальный нетипизированного код, просто добавив аннотацию типа:

(: first : (All (A B) [(Pairof A B) -> A])) 
(define (first p) (p 1)) 
(: second : (All (A B) [(Pairof A B) -> B])) 
(define (second p) (p (ann 2 : 2))) 

Тип конструктора должно быть:

(: make-pair : (All (A B) [A B -> (Pairof A B)])) 

Но конструктор не совсем работает как- является. Одно дело не в том, что в вашем предложении else отсутствует его часть else. Крепление, что дает:

(: make-pair : (All (A B) [A B -> (Pairof A B)])) 
(define (make-pair x y) 
    (lambda (c) 
    (cond 
     [(= c 1) x] 
     [(= c 2) y] 
     [else (error "error in input, should be 1 or 2")]))) 

Это почти правильно, и если наберется ракетка было достаточно удивительным было бы. Типированная ракетка относится к equal? специально для ввода типизации, но она не делает то же самое для =. Изменение = до equal? исправляет его.

(: make-pair : (All (A B) [A B -> (Pairof A B)])) 
(define (make-pair x y) 
    (lambda (c) 
    (cond 
     [(equal? c 1) x] 
     [(equal? c 2) y] 
     [else (error "error in input, should be 1 or 2")]))) 

В идеале появление типирование должно работать с =, но, возможно, тот факт, что такие вещи, как (= 2 2.0) возвращение верно делает, что и труднее реализовать и менее полезными.