[Agda] Positive but not strictly positive types

[Andrés Sicard-Ramírez]

In http://iospress.metapress.com/content/k00w4430j082226w/ (see also
http://basics.sjtu.edu.cn/~yuxi/#publications) Fu gives an
interpretation of positive not strictly positive types in Martin-Löf
type theory.

Is anything "wrong" with Fu's interpretation? I'm asking because it
seems this paper is not cited by the type theory community.

On 11 April 2015 at 10:51, Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
>
> Sent from my iPhone
>
> On 11 Apr 2015, at 01:37, Dan Doel <dan.doel at gmail.com> wrote:
>
> On Fri, Apr 10, 2015 at 5:16 PM, Thorsten Altenkirch
> <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.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Andrés