[Agda] Positive but not strictly positive types

Sun Apr 12 12:12:16 CEST 2015

On 11/04/2015 16:58, "Andrés Sicard-Ramírez" <asr at eafit.edu.co> 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.

Yuxi Fu uses the omega-set model which is a model of the (impredicative)
calculus of constructions. It is not surprising that one can interpret
non-strict positive types here since they can already encoded
impredicatively anyway.

Btw, I have cited him in my PhD but not this paper. :-)

There is nothing wrong with non-strict positive types, classically.

Thorsten

>
>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
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda

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.