headers
Andreas Abel | 1 May 2012 09:51
Picon
Favicon

Re: Re: strict unit type

On 30.04.12 3:36 PM, Vladimir Voevodsky wrote:
>>> PS There is another non-confluent situation with a ->   tt for a
>>> : Pt which does not require dependent sums namely \lambda x:T, f
>>> x where f : T ->   Pt reduces both to f and to \lambda x:T tt .
>>> Both non-confluences can be taken care of by additional
>>> reductions in particular the reduction \prod x:T, Pt ->   Pt for
>>> the example with \lambda.
>>
>> Such a reduction is unhealthy except in the situation where \prod
>> is a "for all" that does not leave marks on the term level.
>
> Well, that was my first thought as well but I am not so sure now. It
> does make it necessary to do some type checking before beta-reduction
> but anyhow the reduction such as a ->  tt for objects of the unit
> type makes reduction context dependent. I have not checked all the
> details yet but it is possible that one can preserve confluence and
> normal form and still have reductions which change the
> sum/prod-structure of type expressions.

I agree that this can likely be modeled, i.e., terms and types can be 
interpreted in a way that these reductions become identities. 
Partially, this is done in Werner et al.'s proof irrelevant model of the 
CIC.

However, I am not so convinced that reduction is the right method in 
this case.  For instance, subject reduction fails unless you work on 
equivalence classes of types.  A more "semantic" approach seems more 
fitting, from my experience.  Also, from the implementor's perspective 
such reductions complicate the picture.  For instance, the problem
(Continue reading)

Permalink | Reply | 2 comments |
headers
Altenkirch Thorsten | 1 May 2012 11:24
Picon
Picon

Re: [TYPES] strict unit type

In general we shouldn't expect to decide eta equality by untyped
reduction. eta equality isa form of decidable extensionality and does not
correspond well to computation to a normal form.

Clearly, the case of the unit type shows that we need to know the type to
check equality.

Trying to decide eta equalities by reduction is very non-modular. This is
basically the point of Vladimir's email.

However, if we implement it as a type directed decision procedure things
are much better. E.g. to terms f,g : Pi x:A.B x are convertible if f x and
g x : B x are convertible (whewre x is a fresh variable) after beta
reduction. Similarily, two terms p,q : Sigma x:A.B x are convertible if
p.1 and q.1 : A are convertible after beta reduction and p.2 and q.2 : B
p.1 (or B q.1) are convertible after beta reduction. (The and here has to
be read sequentially, and the choice B p.1 or B p.2 actually causes some
technical problems).

This is also modular, because we can implement the equality for one type
without having to rethink the equalities at other types.

Thorsten

On 01/05/2012 04:10, "Frederic Blanqui" <frederic.blanqui@...> wrote:

>[ The Types Forum,
>http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>
(Continue reading)

Permalink | Reply | 5 comments |
headers
Benja Fallenstein | 2 May 2012 11:23
Picon

Re: Parametricity is inconsistent with classical logic

Hi all,

On Fri, Apr 20, 2012 at 12:46 PM, Arseniy Alekseyev
<arseniy.alekseyev@...> wrote:
> I've noticed that parametricity postulates are inconsistent with
> classical logic, that is if you postulate both parametricity and the
> law of excluded middle, you can derive a contradiction.

Interesting, I for one hadn't realized that!

If you don't need choice, it seems that you should be able to
circumvent this by using the style proposed by Russell O'Connor in
"Classical Mathematics for a Constructive World":

http://arxiv.org/pdf/1008.1213v2

Since in that approach you don't add any axioms for basic classical
reasoning, there shouldn't be a problem with parametricity.

On the other hand, if you add the classical axiom of choice -- my own
prefered version of writing it would be

> postulate choice : {k l : Level} → {X : Set k} → {F : X → Set l} → ((x : X) → ¬ ¬ F x) → ¬ ¬ ((x : X) → F x)

-- then it seems you'd run into problems again: given

> data Either (X Y : Set) : Set where
>   left : X → Either X Y
>   right : Y → Either X Y
>
(Continue reading)

Permalink | Reply | 16 comments |
headers
Benja Fallenstein | 2 May 2012 11:28
Picon

Re: Parametricity is inconsistent with classical logic

On Wed, May 2, 2012 at 11:23 AM, Benja Fallenstein
<benja.fallenstein@...> wrote:
> [Given classical choice,] you can prove
>
>> tnd : (X : Set) → X ∨ ¬ X
>
> and using choice, you get
>
>> bad : ¬ ¬ ((X : Set) → X ∨ ¬ X)

Ah, this was supposed to read

>> bad : ¬ ¬ ((X : Set) → Either X (¬ X))

of course. Sorry!

- Benja
Permalink | Reply | 0 comments |
headers
Wolfgang Jeltsch | 4 May 2012 17:09

: vs. ∶

Hello,

I propose to not use ∶ in the special syntax for Σ. Sure, it is intended
to be similar to :. However, I think this similarity is precisely its
weakness. You cannot tell from looking at the code whether your code is
syntactically correct or not. Furthermore, there is a semantic problem.
The symbol ∶ is called RATIO, but Σ does not have anything to do with
ratios. I propose to use an alternative syntax, maybe the following:

    syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

What do others think?

Best wishes,
Wolfgang
Permalink | Reply | 25 comments |
headers
Jean-Philippe Bernardy | 4 May 2012 17:24
Picon
Picon

Re: [Agda] : vs. ∶

On Fri, May 4, 2012 at 5:09 PM, Wolfgang Jeltsch
<g9ks157k@...> wrote:
> Hello,
>
> I propose to not use ∶ in the special syntax for Σ. Sure, it is intended
> to be similar to :. However, I think this similarity is precisely its
> weakness. You cannot tell from looking at the code whether your code is
> syntactically correct or not. Furthermore, there is a semantic problem.
> The symbol ∶ is called RATIO, but Σ does not have anything to do with
> ratios. I propose to use an alternative syntax, maybe the following:
>
>    syntax Σ A (λ x → B) = Σ[ x ∈ A ] B
>
> What do others think?

My original intention with 'syntax' was to allow:

syntax Σ A (∀ x → B) = (x : A) × B

(Note the forall, "real" parens and "real" colon).

This could maybe be re-considered.

Cheers,
JP.
Permalink | Reply | 0 comments |
headers
Martin Escardo | 4 May 2012 17:37
Picon
Picon
Favicon

Re: : vs. ∶

I define

record Σ {X : Set} (Y : X → Set) : Set where
  constructor _,_
  field
   π₀ : X
   π₁ : Y π₀

instead. So you have to write Σ {X} Y rather than Σ X Y. On the other 
hand, you can write Σ \(x : X) → Y x, or even Σ \x → Y x when X can be 
inferred. But this would break existing code that uses the libraries.

The ideal solution, however, would be so add Σ, Π, and ∃ as primitive, 
as was done with ∀, so that one can write Σ(x : X) → Y x, or Σ x → Y x.

Martin

On 04/05/12 16:09, Wolfgang Jeltsch wrote:
> Hello,
>
> I propose to not use ∶ in the special syntax for Σ. Sure, it is intended
> to be similar to :. However, I think this similarity is precisely its
> weakness. You cannot tell from looking at the code whether your code is
> syntactically correct or not. Furthermore, there is a semantic problem.
> The symbol ∶ is called RATIO, but Σ does not have anything to do with
> ratios. I propose to use an alternative syntax, maybe the following:
>
>      syntax Σ A (λ x → B) = Σ[ x ∈ A ] B
>
> What do others think?
(Continue reading)

Permalink | Reply | 2 comments |
headers
Andrew Pitts | 4 May 2012 17:53
Picon
Picon
Favicon

Re: [Agda] : vs. ∶

On 4 May 2012 16:37, Martin Escardo <m.escardo@...> wrote:
> The ideal solution, however, would be so add Σ, Π, and ∃ as primitive, as
> was done with ∀, so that one can write Σ(x : X) → Y x, or Σ x → Y x.

I think Jean-Philippe's solution is more ideal than yours---I'd like
to be able to just write (x : A) × B for a dependent product type.

Concrete syntax, don't you just love it...

Andy
Permalink | Reply | 0 comments |
headers
Martin Escardo | 4 May 2012 22:26
Picon
Picon
Favicon

all functions have the same graph


This has probably already been observed by the HoTT aficionados, but I
thought it is sufficiently amusing to post it in this list, with Agda
code linked at the end.

Classical mathematics maintains that a function is the same thing as
its graph. Let's see what happens in type theory.

For f, g : X → Y, define

       graph f = Σ \x → Σ \y → f x ≡ y,

where "≡" of course is propositional equality (identity type). It may
be natural to suppose that, in intensional Martin-Löf theory,

   (*) graph f ≡ graph g → ∀(x : X) → f x ≡ g x.

However, one can show

   (**) univalence → ∀(f g : X → Y) → graph f ≡ graph g.

Because univalence is consistent, and (*) together with (**) proves an
inconsistency (all functions are pointwise equal), we conclude that (*)
is not provable in IMLTT.

Moreover, intensional MLTT cannot deny that all functions have the
same graph.

In particular, the statement "any two functions with equal graphs must
be equal" cannot be used to express extensionality in MLTT, because it
(Continue reading)

Permalink | Reply | 0 comments |
headers
Dirk Ullrich | 5 May 2012 10:14

Fwd: Fix for `geniplate' to build with `template-haskell-2.7.0.0', too

FYI ...

---------- Forwarded message ----------
From: Lennart Augustsson <lennart@...>
Date: 2012/5/5
Subject: Re: Fix for `geniplate' to build with `template-haskell-2.7.0.0', too
To: Dirk Ullrich <dirk.ullrich@...>

Thanks.  I will apply and upload a new version.

On May 5, 2012 2:40 AM, "Dirk Ullrich" <dirk.ullrich@...> wrote:
>
> Hello Lennart,
>
> your Haskell package `geniplate-0.6.0.0' does not build with GHC 7.4.
> This seems to be caused by the `template-haskell-2.7.x' package used
> in this GHC version: `template-haskell-2.7.x' has changed the
> definition of its `Quasi' class. To fix it I've wrapped the
> differences using CPP macros.
> The patch attached contains this change.
>
> I've succeeded to build the patched versions with both GHC 7.2 and
> 7.4. In both case the example program `examples/Main.hs' produces the
> same output like for the unpatched `geniplate'. And the newest version
> of Agda 2 from its darcs repository - using `geniplate' - seems to
> work, too.
>
> Dirk
Permalink | Reply | 2 comments |

Gmane