多型ユニオン型の出現型

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)))でなければなりません。しかし、関数を実装しているときには、が型Aのみを返すことを確認するために何らかの種類の型を入力する必要があるため、(p 1)を直接呼び出すことはできません。 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)条件に失敗したが、それはAのペアのように思えるとBがあります1を与え、Aをバック与える関数、及び2所与は、case->タイプであるB.を関数のこのタイプを表現する方法をバック与える：

#lang typed/racket 

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

アクセサCAコンストラクタの種類があるべき

(: 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ちょうど型注釈を追加することによって、あなたのオリジナルの型指定されていないコードと同じように定義され

(: 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)復帰は難しいの両方を実装し、あまり有用することになるという。