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
?
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>.>) –
@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. –
@JDavidSmith Se si rimuove il caso '#: -', tuttavia, digiterà tipicamente su Racket 6.1.1. –