Nested Paare Übung

Question

Arbeiten durch die ch6 Übungen von Type-Driven Development with Idris,

Übung 3 Zustände:

Wir könnten einen Vektor als verschachtelte Paare implementieren, mit der Verschachtelung von der Länge berechnet. Zum Beispiel:

TupleVect 0 ty =() 
TupleVect 1 ty = (ty,()) 
TupleVect 2 ty = (ty, (ty,())) 

Definieren Sie eine Typebene Funktion TupleVect die dieses Verhalten implementiert. Denken Sie daran, mit dem Typ TupleVect zu beginnen. Wenn Sie die richtige Antwort haben, wird die folgende Definition gelten:

test : TupleVect 4 Nat 
test = (1,2,3,4,()) 

Hier ist, was ich kam mit:

TupleVectType : Nat -> (a : Type) -> Type 
TupleVectType Z  _ =() 
TupleVectType (S n) a = (a, TupleVectType n a) 

TupleVect : (n : Nat) -> a -> TupleVectType n a 
TupleVect Z _  =() 
TupleVect (S n) a = (a, TupleVect n a) 

Ich dachte, dass es war ausreichend, aber MyTupleVect 4 Nat falsch ist :

*Exercises> TupleVect 4 Nat 
(Nat, Nat, Nat, Nat,()) : (Type, Type, Type, Type,()) 

Aber, also nicht eine Type wenn ich einen tatsächlichen Wert bieten, retur es ns:

*Exercises> TupleVect 4 True 
(True, True, True, True,()) : (Bool, Bool, Bool, Bool,()) 

Bitte teilen Sie mir, wie Sie diese TupleVect Funktion zur Korrektur der erwarteten Ausgabe anzupassen.

Es ist mir nicht klar, wie TupleVect 4 Nat, zur Verfügung zu stellen und dann aufzählen, die Nat ‚s, aber 1 beginnen, nicht 0.

Answer 1

Ihre Definition von TupleVectType ist eigentlich was TupleVect sollte. In der Übung werden Sie aufgefordert, eine Funktion TupleVect zu implementieren, die den Typ von n -are Tupel-dargestellte Vektoren zurückgibt.

Deine Definition von TupleVect ist eine Implementierung von dem, was gemeinhin replicate genannt wird, die ein einzelnes x : a auf einen Vektor nimmt repeat x : Vect n a durch n mal zu replizieren.

Zusammengefasst mit Definitionen, die folgenden typechecks wie erwartet:

foo : TupleVectType 4 Nat 
foo = (1, 2, 3, 4,()) 

so würde ich raten nur TupleVectType zu TupleVect umbenennen.