다형성 유니온 유형으로 발생하는 입력

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에 대한 조건자를 사용하는 방법)에서 입력 형식을 사용하여 쌍의 첫 번째 구성 요소 만 안전하게 반환 할 수 있습니다.

UPDATE는 I 위에서 약간 다르며 make-pair 함수 인수로 공급 될 A 및 B위한 조건을 필요로하는 방법을 시도했다. 아래는 코드입니다

#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"))))) 

그러나,이 질문의 시작 유형이 지정되지 않은 코드에서 오류 expected: A given: (U A B) in: f-value

Answer 1

와 체크 (fn-pred f-value) 상태에서 실패는, 그것은 한 쌍처럼 보인다와 B는 것입니다 1을 받아, 다시 제공 기능, 2 소정는 case-> 유형이다 B.에게 함수의 유형을 표현하는 방법을 다시 제공한다 :

#lang typed/racket 

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

되는 접근 캘리포니아

(: make-pair : (All (A B) [A B -> (Pairof A 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))) 

생성자의 형식이되어야합니다 : N 단지 형 주석을 추가하여, 원래 형식화되지 않은 코드와 동일한 방법으로 정의 할 수 입니다. 한 가지 잘못된 점은 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) 복귀는 힘들어 모두 구현하고 덜 유용 할 수 있음을 수있다.