module Spine: Generic_view_spine
The type is a GADT. The constructor App
uses an
existential quantification for the type of the argument. The
representation of the argument type is useful when defining
generic computations over a spine.
module T:sig
..end
type'a
t ='a T.spine
c(v0,...vn)
to the form App (....(App (c', t0, v0)..., tn, vn)
where tk
is the representation of vk
's type.
and c' = Con (c\_desc, fun x0 ... xn -> c(x0,...,xn)
.
In essence, the spine view of a value gives a data constructor and a list of all its arguments together with their types.
<<spine view constructors for int lists>>=
let nil = Con (nild, [])
and cons ty hd tl =
App (App (Con (cons_desc, fun x y -> x :: y), ty, hd)
, List ty, tl)
@
val spine : 'a Ty.T.ty -> 'a -> 'a T.spine
val view : 'a Ty.T.ty -> 'a -> 'a T.spine
val rebuild : 'a T.spine -> 'a