Only the first constructor needs to be inspected:The first type parameter is the type of the first element in either algebraic data type. The source examples therefore return
headZig :: Zig a b -> a
headZig (Cins x _) = x
headZig Nil = error "headZig: empty input"
headZag :: Zag a b -> a
headZag (Cans x _) = x
headZag Nal = error "headZag: empty input"1 and "C", respectively. These functions are partial at empty inputs, as allowed by the stated nonempty-input requirement.The constructors For example,
ZigType and ZagType record which of the two alternating positions contains the last element. The tail types swap the two type parameters, so the return type of lastZag swaps them back:lastZig :: Zig a b -> ZigOrZagType a b
lastZig Nil = error "lastZig: empty input"
lastZig (Cins x Nal) = ZigType x
lastZig (Cins _ zs) = lastZag zs
lastZag :: Zag a b -> ZigOrZagType b a
lastZag Nal = error "lastZag: empty input"
lastZag (Cans x Nil) = ZagType x
lastZag (Cans _ zs) = lastZig zslastZig passes a tail of type Zag b a to lastZag, whose result then has type ZigOrZagType a b, exactly as required. Conversely, lastZag passes a Zig b a tail to lastZig. A singleton returns its element in the appropriate constructor; a longer input discards one element and uses mutual recursion on the shorter tail. This proves correctness by structural induction on the finite alternating sequence. The three source examples give ZigType 2, ZagType "D", and ZigType True.In the first expression, pattern matching discovers that the first tail is nonempty, so the ignored first label, the bottom value , is never demanded. The singleton
Cans 'A' Nil returns ZagType 'A'.In the second expression the tail is
Nal, so the result is ZigType applied to the bottom value. Under lazy evaluation this has a defined outer constructor and an undefined field: case lastZig (Cins undefined Nal) of ZigType _ -> True yields True, whereas extracting or fully printing the payload fails. Thus the result is , not a wholly undefined outer value.The original PDF really prints
Nil in the third expression. Cins requires a tail of type Zag b a, whereas Nil has type Zig c d. These distinct type constructors cannot be unified. There is no well-typed expression to evaluate, regardless of the undefined first label; replacing Nil by Nal would change the question.Map each current first-position value with the first function, then swap the functions when descending to the other algebraic data type:All four type variables are independent: mapping may change both element types. There is no
mapZig :: (a -> c) -> (b -> d) -> Zig a b -> Zig c d
mapZig _ _ Nil = Nil
mapZig f g (Cins x zs) = Cins (f x) (mapZag g f zs)
mapZag :: (a -> c) -> (b -> d) -> Zag a b -> Zag c d
mapZag _ _ Nal = Nal
mapZag f g (Cans x zs) = Cans (f x) (mapZig g f zs)Enum or numeric constraint on the mapping functions themselves; constraints arise only from particular arguments such as succ or (+2). The mutual recursion preserves every constructor and applies the intended function at each alternating position. The results are Cins 3 (Cans 'B' (Cins 4 Nal)) and Cans "D" (Cins True (Cans "E" Nil)), respectively.Use the symmetric tree fold equations for the other algebraic data type:The most general type signatures, using the same schematic variable names independently for each function, areFor
foldZag (fZag,eZag) (fZig,eZig) Nal = eZag
foldZag (fZag,eZag) (fZig,eZig) (Cans x z) =
fZag x (foldZig (fZig,eZig) (fZag,eZag) z)foldZig :: (a -> s -> r, r) -> (b -> r -> s, s)
-> Zig a b -> r
foldZag :: (a -> s -> r, r) -> (b -> r -> s, s)
-> Zag a b -> rfoldZig, the first empty value has type r, so the first combining function must return r. Its label argument has type a. The recursively folded tail has some independent result type s, giving a -> s -> r. The second combining function consumes a b label and an r result and returns s, giving b -> r -> s. The second empty value has type s. Swapping the two handler pairs and the label types makes the recursive call well-typed. The identical argument applies to foldZag.The two result types need not coincide. For example, one handler can return an integer and the other a list; forcing both results to have one type would lose parametric polymorphism allowed by the definitions.
Articles by others on the same topic
There are currently no matching articles.