Sebastian Hanowski wrote:
Maybe it's just Epigram running out of RAM on my machine. But since
freeing the program shed by shed was so easy i got nervous in the
all-at-once case.
Ah, that old thing...
from the programmer. Moreover, an improved language design would
provide some means to access information which is present in the
context but not showing up in patterns...
You mean like the 'where' for Epigram 2 you introduced when you blogged
about views for equality?
Exactly. The idea might be something like this; you just write a bunch
of declarations in the where clause
a : Nat; b : Nat; p : Le a b
or whatever. The semantics is inevitably ambiguous: there where clause
is ok if the declarations can be mapped injectively to context entries
not explicitly bound in the lhs. This ambiguity is both inevitable and
appropriate: you get out the information you put in.
In fact, there's a generalisation of this which I quite fancy trying
out. For a long time, James McKinna has wanted to experiment something
like Dyckhoff's algorithm jacked up to dependent types. Inevitably,
completeness goes out the window, but we only want to hire some help
with the cut-free drudgery, not to get made redundant, right? The other
thing that's potentially nice in this setting is that you can
'configure' the search by throwing in more copies of stuff which is
going to be needed more often, not called for in the propositional case
where you never need the same assumption twice on any one branch of the
tree, but now the same assumption can be given distinct uses.
I can think of and have been in a situation where i'd like the system to
commit a profound context access:
Isn't elaborating a shed with a call to an undefined function (e.g. at
the top) the same as stating a programming problem? The required return
type follows from the context, the hypothesis follows from arguments and
their types and you've just given a call pattern.
That's a good idea. You're not alone in asking for this. The type
inference picture isn't quite as rosy as you hope, but it's still pretty
good. It's like this, suppose we're at
...; x:X; y:Y; z:Z; ... |- [h x y z] : T
for some unknown h. We may readily introduce an incomplete defnition for
h : all x:X; y:Y; z:Z => T
Of course, we have to populate this binder prefix with any implicit
stuff that shows up in the types, but that ain't so hard, I suspect. The
point is, we can build the type if we only generalise over distinct
variables (or, strictly speaking, the Miller-patterns induced by the
available eta-laws). These are 'most general arguments', hence you can
compute the whole of the range; if you start with h zero : T, you have
no idea what should be the type of h (suc n). But if we can't build the
type, we can certainly ask for it, filling in as much as we can, and
constraining the result by usage.
I'm not sure yet if this generalizes nicely or even would be a sensible
operation at all, but instead of overstriking the call with yellow,
wouldn't it be possible to pack things up and initialize a new line with
them further up the script? That would save a whole lot of typing and
probably an undo, because usually all things yellow need to be undone to
get back their context such that you can see what's precisely missing.
Where this function gets shoved is an interesting question. I think it
should go *locally* in the where clause. However, it should also be
possible (by some refactoring/lambda-lifting cheekiness) to move it
outwards from the where clause. Thank you, Simon Thompson!
All of this will happen sooner or later...
Cheers
Conor
