Agda: Return Kopf und Schwanz der leeren Liste

Ich lerne Agda und üben auf Listen, um ein besseres Verständnis zu bekommen. Im Moment versuche ich Funktionen für die Liste zu schreiben. Ich bin verwirrt darüber, wie man den Kopf und das Ende einer leeren Liste zurückgibt. Hier ist mein Code:Agda: Return Kopf und Schwanz der leeren Liste

data list (A : Set) : Set where 
[] : list A 
_∷_ : A → list A → list A 

Null : {A : Set} → (list A) → Bool 
Null [] = true 
Null (x ∷ a) = false 

tail : {A : Set} → (list A) → A 
tail [] = {!!} 
tail (x ∷ []) = x 
tail (x ∷ a) = tail a 

head : {A : Set} → (list A) → A 
head [] = {!!} 
head (x ∷ a) = x

Eine Arbeit um, dass ich festgestellt, dass statt der ersten und letzten Mitglieder der Rückkehr ich eine Liste zurück, die ersten und letzten Elemente enthält, die sich wie folgt:

tail : {A : Set} → (list A) → (list A) 
tail [] = [] 
tail (x ∷ []) = x ∷ [] 
tail (x ∷ a) = tail a 

head : {A : Set} → (list A) → (list A) 
head [] = [] 
head (x ∷ a) = (x ∷ [])

Aber ich bin immer noch verwirrt darüber, wie man die Werte für Kopf und Schwanz zurückgibt. Wie kann ich das machen?

P.S Keine Zuweisung. Meilen vor diesem Zeug in der Klasse

Quelle

2017-02-16 danny

Die leere Liste nicht Kopf und Schwanz hat. Du kannst keine Dinge zurückgeben, die nicht existieren. –

@ AndrásKovács Bedeutet das, dass ich nie eine Funktion wie diese in Agda schreibe? Gibt es eine andere Arbeit als die Rückgabe einer Liste? – danny

In Agda ist der Typ einer Funktion sehr wörtlich zu nehmen. Eine 'A -> B'-Funktion gibt ein' B' für jedes 'A' zurück, und es wird niemals eine Schleife gemacht, es wird niemals eine Ausnahme geworfen, es wird niemals etwas anderes als ein' B' zurückgegeben. Wenn Sie feststellen, dass ein Typ keine Implementierung hat, müssen Sie den Typ ändern. In diesem Fall können Sie 'head: {A: Set} -> Liste A -> Maybe A' verwenden oder' Vec' von 'Data.Vec' verwenden, die' head' und 'tail' für nichtleere Vektoren unterstützt. –

In Agda, Funktionen sind insgesamt: Wenn Sie head : {A : Set} -> list A -> A haben, dann muss es über alle Listen definiert werden. Doch für head [] können Sie nicht ein Element für einige willkürliche Art A (man stelle sich head ([] : list Void) ...)

Das Problem ist, dass Ihre Art von head verspricht zu viel zaubern. Es ist in der Tat nicht wahr, dass Sie das erste Element einer Liste zurückgeben können. Sie können es nur für nicht leere Listen tun. Sie müssen also head ändern entweder ein separate proof von nicht emptiness nehmen oder ein non-empty list als Argument zu nehmen:

module SeparateProof where 
    open import Data.List 
    open import Data.Bool 
    open import Data.Unit 

    head : {A : Set} → (xs : List A) → {{nonEmpty : T (not (null xs))}} → A 
    head [] {{nonEmpty =()}} -- There's no way to pass a proof of non-emptiness for an empty list! 
    head (x ∷ xs) = x 

module NonEmptyType where 
    open import Data.List.NonEmpty hiding (head) 

    head : {A : Set} → List⁺ A → A 
    head (x ∷ xs) = x -- This is the only pattern matching a List⁺ A!

Quelle

2017-02-17 03:26:30 Cactus

Agda: Return Kopf und Schwanz der leeren Liste

Antwort

Verwandte Themen