Talk:Implicit and explicit parameters

From The Twelf Project
Jump to: navigation, search

Universal quantification

Is the implication supposed to be that only implicit parameters are universally quantified? In the type theory, both are exactly the same: Πs. I think this may be misleading. (Or is there some interpretation in logic programming that I'm missing?)  — Tom 7 13:35, 16 October 2006 (EDT)

No, you're right - seems like the right way to say it is that this is two different ways to do universal quantification, in fact. — Rob (and his talk) 11:26, 12 November 2006 (EST)

This article or section needs a moral stand

Is there a reason that this article doesn't say "don't use explicit parameters unless there is a good reason to; here are the only good reasons: {termination, mode}"? Drl 20:29, 14 March 2007 (EDT)

  • Well, I think there are good stylistic reasons to use explicit parameters (much like it is sometimes good style to use explicit type annotations or explicit quantification in SML) which are hard to circumscribe. I'd rather describe it in terms of pros and cons. (And actually, I don't think %mode is even necessarily a good reason, since it is possible to give modes to implicit arguments.)  — Tom 7 21:43, 14 March 2007 (EDT)
  • I would be inclined to agree, in that we should take "moral stands" where such are clear - don't start constants with capital letters, don't define an inductive notion of equality when what you mean is identity on LF terms. However, the article should probably say "we usually default to this style," which is what I tried to say. — Rob (and his talk) 22:20, 14 March 2007 (EDT)

Always prints out the parameters

I don't think it's true that Twelf always prints out the implicit parameters. For example, I think that implicit parameters to parameters are not always shown? This is why sometimes you see a {A:typ} where A appears nowhere else. Does anyone understand the actual rules? (Jason?)  — Tom 7 17:01, 26 October 2007 (EDT)

It prints out implicit parameters but not implicit arguments. I think this demonstrates the {A:typ} thing, I think I should change the example to something more like this. — Rob (and his talk) 11:55, 28 October 2007 (EDT)

tp : type.
tp/unit : tp.

exp : tp -> type.
unit : exp tp/unit.
abort/1 : exp A.
abort/2 : {A} exp A.
step : exp A -> exp B -> type.

step/raise : step unit abort/1.

step/raise : step unit (abort/2 A).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on

step : {A:tp} {B:tp} exp A -> exp B -> type. step/raise : {X1:tp} step unit abort/1. step/raise : {A:tp} step unit (abort/2 A).

%% OK %%
What's the difference between an implicit argument and an implicit parameter? Or you mean, it always prints out the implicit Π bindings, but never the implicit occurrences? Anyway, yes, I think this is a good example.  — Tom 7 18:47, 28 October 2007 (EDT)