[Agda] Positive but not strictly positive types

[Dan Doel]

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 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.

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.

-- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150410/8d3a821e/attachment.html