[Agda] Positive but not strictly positive types

Sun Apr 12 10:25:46 CEST 2015

Andres, thanks for the pointer.  I had never come across Fu's work.

On p5/6 (Section 3.1) he interprets strictly-positive inductive types as 
the limit of a sequence of approximations (as I do with sized types). 
In Section 5 he says nothing changes if "strict" is dropped.

However, he does not give an argument why the limit in 3.1 exists, i.e., 
he does not give a closure ordinal.  It is highly likely that the 
closure ordinal grows (drastically!?) when dropping strictness.  I 
always just use the first uncountable ordinal, a sledgehammer that is 
big enough...

Thorsten does not believe in classical ordinals so he will likely reject 
Xu's justification.

Cheers,
Andreas

On 11.04.2015 17:58, Andrés Sicard-Ramírez wrote:
> 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
>>
>
>
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/