[Agda] Positive but not strictly positive types

Sat Apr 11 17:51:46 CEST 2015

Sent from my iPhone

On 11 Apr 2015, at 01:37, Dan Doel <dan.doel at gmail.com<mailto:dan.doel at gmail.com>> wrote:

On Fri, Apr 10, 2015 at 5:16 PM, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk<mailto:Thorsten.Altenkirch at nottingham.ac.uk>> wrote:

Ah indeed, I thought this was a bit of a dejavue. I have to admit that I haven’t digested your code. I always thought that Church encodings are not very practical.

They are very practical for some things and impractical for others, which is also true of the way we usually think of data/inductive types being implemented (often where one is practical, the other is impractical). Although typically one would think that zipping is an impractical case for encodings, it turns out not to be the case if one has positive types (positive data-like types, at least; I haven't worked through whether encodings of positive types get you the same performance increase here).

I don't really understand what, "the only justification is classical," means. System F has non-strict positive types. Is it classical?

I’d say so because the only justification for impredicativity is that Prop is small because Bool=Prop.

I still don't know what "justification" means.

I care about them inasmuch as I'd be interested in seeing a system that allowed them, so I could see what kinds of programs they'd be useful for, and what tradeoffs would have to be made to avoid breaking various properties of the system. From the above, it seems like they have uses when you're doing things with continuation passing.

And if "justification" refers to the existence of some particular sort of model, I basically don't care about that at all. So positive types would automatically win that fight for me.

If you just want to program you can switch off positivity checking.

I could, but then I wouldn't know whether I could accidentally do something 'bad' that I do care about, like write a non-terminating program, or end up in a situation where canonicity or subject reduction fails. So it is also in my interest to encourage other people's interest in studying systems specifically designed for having positive types along with the other nice properties, and studying which other features don't combine with it. That way I don't have to do it (all) myself.

And it is also in my interest to complain at people discouraging such study because such systems aren't "justified." :)

I am not discouraging anything. However I think for programming purposes it is enough to work in a dependently typed programming language which one can do in Agda by switching off the termination checker.

Extending the collection of total programs would in my view require some justification. I'd rather hope that this isn't necessary and that you can achieve what you want without extending type theory.

I didn’t refer to “some sort of model” but just some naïve understanding. Strictly positive types model some sort of trees, I have no idea what non-strict positive one are. The justification seems just formalistic.

Formalism is fine by me. I'm telling a computer to push around symbols until it spits out a bunch of symbols in the form I want. The problems come when an addition prevents that from happening. It's fine if there are things that aren't trees as long as when I have something that is supposed to be a tree, it's actually a tree, even if I used non-trees to get there.

I don't buy this. When you write a program you should be able to explain why it works. This has nothing to do with computers.

Usually we get non-strict positivity when we apply the negative translation (aka CPS translation) to an inductive (or coinductive) definition. It is not clear to my why those should exist from a constructive point of view.

"Should" sounds like "justification." Like we have some other system that we've decided is constructive, and we're trying to decide whether something else is constructive by whether we could do all the things in our original system.

But I guess I am a formalist, because I don't see why everything doesn't simply 'exist' by fiat, and then we look at properties of the system (like the disjunction and existence properties, or canonicity) to determine if it's constructive, and care about those properties because they work the way we want. This goes for strictly positive types, too; they exist because we said they exist when we defined the system. And if impredicative polymorphic types exist, that's very nice, too, because it gives very direct ways of internalizing universal constructions. The only problem to me is that when you add together too many of these nice things in the wrong way, other nice things go away.

Like a child in the sweetie shop :-)

I agree that we have to experiment with things we don't understand yet in order to understand them. Such an understanding can either lead to the insight that we can justify them in the existing framework or that we need to extend the framework.

-- Dan

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150411/85010551/attachment-0001.html