2015-03-19 15 views
5

Sto cercando di definire il tipo di annotazione per la seguente funzione nel tipizzati Racket:Rappresenta la funzione EOF -> False, A -> A ∀ A ≠ EOF in Racket tipizzato?

(define (neof x) 
    (if (eof-object? x) #f x)) 

Lasciando non-annotato dà il tipo:

(Any -> Any) 

Utilizzando questo tipo genera un errore:

(: neof (All (A) (case-> 
        (EOF -> False) 
        (A -> A : #:+ (! EOF)))) 

    expected: A 
    given: False 
    in: #f 

Questo è presumibilmente perché si può lasciare A = EOF e quindi si ottiene EOF -> EOF.

Il tipo (: neof (All (A) A -> (U A False) #:- (U EOF False))), pur non essendo chiaro come quanto sopra, dà anche errori:

mismatch in filter 
    expected: (Top | Bot) 
    given: ((! (U False EOF) @ x) | ((U False EOF) @ x)) 
    in: (if (eof-object? x) #f x) 

Il mio obiettivo era quello di avere una funzione che ho potuto applicare a qualsiasi uscita da una porta di ottenere sia False o valore dalla porta. Ora sto riconsiderando la necessità di questo, dato che ho perso troppo tempo a cercare di capire questo tipo.

Per completezza, ho anche provato questa definizione di neof:.

(define/match (neof x) 
    [((? eof-object?)) #f] 
    [((? (compose not eof-object?))) x]) 

(anche con il secondo modello essendo _, ma che non codificare la stessa quantità di informazioni di tipo A questo punto sono più cercando di placare il type checker di qualsiasi altra cosa).

Quindi: come posso rappresentare il tipo di neof?

risposta

3

Penso che il tipo che si desidera è questo:

(: neof (All (A) (A -> (U False A) : 
        #:+ (! EOF) 
        #:- (or EOF False)))) 

(La clausola #:- è opzionale, ho appena incluso lì per completezza.)

Nota: Se la clausola #:- è incluso, sarà non typecheck in Racket 6.1.1. La rimozione della clausola consentirà il passaggio 6.1.1.

Il problema qui è che tutti i rami di case-> devono corrispondere a in modo indipendente l'uno dell'altro. Per il caso (A -> A), non riesce perché #f non è un A. Le informazioni di digitazione dell'occorrenza dal primo caso non possono influenzare il controllo della digitazione sul secondo caso.

+0

La tua risposta sembrava buona, quindi ero davvero fiducioso. Sfortunatamente, questo è il risultato: 'Controllo tipo: mancata corrispondenza di tipo; errata nel filtro previsto: ((! EOF @ x) | Bot) \ n dato: ((! (U False EOF) @ x) | ((U False EOF) @ x)) \ n in: (if (eof-object? x) #fx) ' (\ n sono aggiunti da me, theyr'e ​​newlines che i commenti non possono avere>.>) –

+0

@JDavidSmith Hmm, hai ragione, non tipografico per me su Racket 6.1.1. Typed Racket è attualmente in uno sviluppo piuttosto pesante, quindi questo è qualcosa che sembra solo tipografare sugli snapshot. È possibile scaricare una [configurazione snapshot] (http: //pre.racket-lang.org/installatori /), se lo desideri, di solito sono piuttosto stabili. In caso contrario, potrebbe essere necessario attendere fino alla prossima versione. –

+0

@JDavidSmith Se si rimuove il caso '#: -', tuttavia, digiterà tipicamente su Racket 6.1.1. –