Serguey,
A reasonable question, to which you might receive several possible answers:
At the risk of duplication, or just being a bit out of date now --- the
previous go having failed as I needed to re-align my subscription
address to my new coordinates --- let me add the following observations
below.
Thanks for your continuing interest, and I hope this helps, (and perhaps
my other colleagues will leap in to correct or contradict me!)
James McKinna
Radboud University Nijmegen
Serguey Zefirov wrote:
I hardly can find any example of higher-order functions in Epigram
examples. I searched distribution examples and online examples.
Why is that?
0) on the language and its library of examples
0a) the library, such as it is, has been focused on examples which show
off the use of indices in type families to constrain computation:
typically, these take the form of first-order data (lengths of vectors,
size bounds on trees, type names...) used for measurement
0b) incidentally, the use of 'by' notation hides a lot of
behind-the-scenes dependently-typed higher-order functions... actually,
I don't think this is (co-)incidental at all --- see 3) below
1) on higher-order functions proper
1a) standard higher-order functions such as map, fold on lists etc. are
all trivially available (and/but simply-typed!), so not much attention
has been paid to them; functions which take dependently-typed functions
as arguments are less common in nature or experience --- we are still
learning to program this way. But you could try writing the version of
"map" which takes a list of elements of A, a function f of type
(x:A)B(x) which ensures each a in A is mapped to ... something
satisfying property B, and returns a function mapping lists of As to
lists of "elementwise B(-)s". If you were to try this example, it might
throw up some interesting problems: should the result type be List
(Sigma a:A. B[a]) or something more interesting? And then how do you
write the function? Choices, choices, ...
1b) [Wouter's suggestion also includes this example] for a non-trivial
example of a dt higher-order function, look at Conor's draft paper on
closure under substitution in syntax with binders (I can probably supply
a URL if you need it); we need more examples like this: in this case,
the proofs were done years ago (by myself and Healf Goguen), and the
programs re-invented in a slightly different way, only years later...
2) on a syntactic restriction
Epigram 1's syntax for let declarations and their bodies discourages
writing functions which return functions ... e.g. Epigram 1 doesn't
allow terms of the form
lam x => case x { ...} for example: case x is an elimination operator,
so is expected to appear in a <= expression. Taking functional
arguments is no problem, though, and they can even be declared
inference-rule style...
3) more speculatively, more abstractly
You might wonder about higher-order functions in the special case of
parametric polymorphism in simply-typed languages: do they impose a
uniformity on their use/application (or the use of their h-o arguments)
which runs counter to the 'learning-by-testing' which arises in
dependently-typed case analysis? What are the right ways to capture new
kinds of such uniformities in the dependently-typed case? Again, only
examples and experience will tell us. Here example 1b above is a good
such candidate (sorry for the pun): h-o functions which carry around
functional arguments representing abstract closure conditions on the
intended source and target data. Elimination operators (0b above) are
just one very general vision of that idea: for 'methods' in elimination
operators are just 'abstract closure conditions which correspond
to/arise from patterns of data' (typically, but not necessarily, given
by constructor patterns).
