Redesign arithmetics support

[Toxaris]

@plmday is not happy about the current arithmetics support (see comment on 1ed3eaef2c71116ee6d06bfe0aaba03b238d1d70). In particular, the built-in type for arithmetics is called Nat but behaves like Haskell's Integer.

If we touch this, we should also fix div. It has two problems: It needs to round down its result, and it is partial because of division by zero.

[reflectionalist]

I found the current implementation of div reasonable. I especially like the return value for 1 div 0 which is itself, rather than some horrible error.

[reflectionalist]

The earlier renaming Int to Nat is just a temporary solution. It is still not satisfactory. In particular, subtraction could still leak into the negative world. Although it can be easily fixed, the support for natural numbers is still weak. In particular, we offer the user no way of defining interesting functions.

I plan to completely migrating into Peano numbers (internally represented using Hasekll integers), including support for two constructors Z (for zero) and S (successor), and one recursor R for defining recursive functions, meanwhile, still offering add, sub (but force it to zero or stuck when subtracting a larger natural number from a smaller), mul and div (forcing it to stuck when diving a number by zero) for efficiency considerations.

[Toxaris]

Proper support for naturals (including recursion) sounds good.

If you planned the huge rename to be temporary, you could have mentioned that.

What about supporting both Int and Nat?

[Blaisorblade]

@plmday, I'm confused - you say "The earlier renaming Int to Nat is just a temporary solution. It is still not satisfactory. In particular, subtraction could still leak into the negative world." but you did the opposite renaming, and subtraction was just fine with that.

If you want Peano naturals, maybe it'd be cool to support directly ADTs (which might be needed anyway for integration with SugarFomega).

[Toxaris]

If I understand correctly, SugarFω natively supports products, sums, and iso-recursive types. Datatype syntax à la Haskell or ML is provided as syntactic sugar on top of that.

[Blaisorblade]

So, at least eventually, you'd want to implement "that" (i.e., something equivalent to ADTs, like products, sums and types). Then, naturals could be implemented on top of "that".

IMHO, one could implement naturals meanwhile anyway - we are not guaranteeing source compatibility (yet) or anything like that. You could require an import statement to use Peano naturals, and the module could for now just enable naturals with a built-in "pragma", and in the future instead define those combinators.

But it might be cooler to just catch up with the base features of SugarFω.

[Toxaris]

I would like to somehow integrate such additional features into the notion of "PTS instance". So for example, a user should be able to select a language such as "System F, with natural numbers on the type level, and coproducts on the term level".

[Blaisorblade]

natural numbers on the type level

Cool! You could have all that with extra command line options, but clearly we can't hardcode all interesting choices in the source - your example clarifies that you don't want standard choices (say, PCF and CIC) but just all possible choices.

I must have already argued that instances should be definable within programs. But to allow such combinations, you want a small combinator language for defining instances within programs by, say, mixing in extensions on base languages.

I also suggested that you should be able to add extensions to a language using a bigger language. Hence, you could implement type-level naturals as a library in, say, (some subset of) CIC, and then import them in a smaller language. If this sounds too crazy, think of defining lists in Fω and importing them as constants in STLC: sounds sensible, doesn't it?

The only unclear part (to me) is how to turn Fω's List : * -> * into a builtin type constructor - a syntactic form for types (STLC doesn't have type application, so importing it as a type constructor isn't enough). But e.g. yesterday's paper did not define an Fω but still had type constructors, so that might be OK: we might just restrict abstractions, not applications.

Also, one uses smaller languages for their stronger meta-theoretic properties, which you can lose given these extensions. But I'd avoid caring: if you import something that breaks soundness, you're on your own, since whether you keep soundness is undecidable.

And at some point, such an implementation maybe becomes a "tool paper" somewhere (especially with type inference), so that users can cite it, or maybe some kind of experiment. But whatever.

But let's please not kill this by feature creep and keep it agile, even though I know I'm the guiltiest right now.

[Toxaris]

As a first step, I envision some form of combinator library to create values of PTS.Instances.PTS, that is, language descriptions. For example, could we have a Monoid instance?

In the future, we could add an external syntax for the combinators.

[Blaisorblade]

Semigroup sounds obvious, but Monoid requires an empty instance. Which is possible: it would just contain no sorts.

[Toxaris]

It would indeed by easy to merge the sorts, but what about the axioms and relations? Is the composition of two functional pure type systems still functional? (In a functional pure type system, the third position in the relations is determined by the first two positions).

[Blaisorblade]

Is the composition of two functional pure type systems still functional?

I don't think so - a counterexample should be easy to construct (take a PTS where a lambda-abstraction is a type, that is a relation (*, *, **), and merge it with a more standard PTS).

But take two PTS instances i1 and i2, and assume that in both i1 and i2 we have P(i) = "in PTS instance i, every possible abstraction has the same sort as its body" (the common case, rules out the previous counterexample). Then we also have P(i1 merge i2). Moreover, P(i) implies that i is functional.

Are there PTS where P doesn't hold? I guess so, but I'm not sure what's the point.

However, it might be easier to use, for each field, the Monoid instance for Maybe (Last t).

[Toxaris]

Consider the following PTS:

Sorts = *, **, ***
Axioms: *:***, **:***
Relations: (*,*, **)

If I got it right, this is a language that supports abstraction over values (that is, the PTS supports first-order functions), but not abstraction over functions (that is, the PTS does not support higher-order functions'). Note that * is the kind of non-function types, ** is the kind of function types, and *** is the sort of proper kinds. Compare with GHC's Rank2Types language extension (which is not the same thing as this example, but propably expressible as a PTS by shifting the example one level).

[Blaisorblade]

Cool! I was thinking of

Axioms = {* : **}
Relations = {(*, *, **)}

where P doesn't hold, but which seems even weirder.

Anyway, back to the main question, if you want to support this kind of PTS, maybe the Monoid instance shouldn't merge axioms/sorts/relations. But I propose something like 'mergeStandardPTSs`, where "standard" should be replaced by a word which describes P (while "standard" is something I just made up).

[Blaisorblade]

This issue got diverted away — the latest discussions are in #114. Hence closing.