Bekannte Mustererkennung in agda

Grob gesagt, ich habeBekannte Mustererkennung in agda

check : UExpr -> Maybe Expr

und ich habe einen Test Begriff

testTerm : UExpr

die ich check erfolgreich hoffen, nach dem ich die resultierenden Expr extrahieren möchte und manipulieren es weiter. Grundsätzlich

realTerm : Expr 
just realTerm = check testTerm

Derart, dass diese Definition auf typecheck würde scheitern, wenn check testTerm stellte sich heraus, nothing zu sein. Ist das möglich?

Quelle

2016-09-14 luqui

Sie könnten [Eliminating a Maybe auf der Typenebene] (http://stackoverflow.com/questions/31105947/eliminating-a-aybe-at-the-type-level) nützlich finden. – user3237465

Im Gegensatz zu den technischen Antworten unten möchte ich darauf hinweisen, dass Sie nicht funktional denken. Es ist wie jemand, der die "IO" -Monade loswerden will und überall in Haskell Imperativcode schreibt: Im Allgemeinen gibt es keine Möglichkeit, den zugrunde liegenden Typ aus einem Begriff vom Typ "Maybe" zu extrahieren; Es ist der Kern starker funktionaler Programmiersprachen wie Agda, also musst du die Monade so lange herumreichen, bis du einen guten Weg gefunden hast, sie in einen Wert eines anderen Typs zu codieren. –

Das übliche Angebot etwas wie

Just : {X : Set} -> Maybe X -> Set 
Just (just x) = One -- or whatever you call the fieldless record type 
Just nothing = Zero 

justify : {X : Set}(m : Maybe X){p : Just m} -> X 
justify (just x) = x 
justify nothing {()}

schreiben Wenn m zu einem Erfolg berechnet, ist die Art von p Eins und der Wert abgeleitet wird.

Quelle

2016-09-14 07:17:16 pigworker

Ich hatte gerade angefangen, dieses Idiom mit 'True' zu sehen, aber ich habe mich nicht wirklich vergraben. Danke. – luqui

Nun, ich habe einen Weg gefunden, es zu tun, der so skurril und magisch ist.

testTerm-checks : Σ Expr (\e -> check testTerm ≡ just e) 
testTerm-checks = _ , refl 

realTerm : Expr 
realTerm = proj₁ testTerm-checks

Dies gibt mir die Heebie Jeebies, aber nicht unbedingt in einer schlechten Art und Weise. Immer noch an anderen Möglichkeiten interessiert, es zu tun.

Quelle

2016-09-14 07:17:24 luqui

Bekannte Mustererkennung in agda

Antwort

Verwandte Themen