Questions - Agda

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Sam Toth

Hi, beginner here working through PLFA. Would anyone be able to help provide an intuition on why function extensionality is not provable from within Agda. I’ve heard that it is possible with cubical agda - but i don’t have a good grasp on what that is yet. I’ve also heard agda’s type system described as intentional whereas others are extensional. Does this have anything to do with function extensionality or are they unrelated?

Georgi Lyubenov // googleson78

it's "not true" in a sense - the traditional thing called equality in agda is "it's actually the 'same' thing", while that's not necessarily true for two functions that match pointwise

Georgi Lyubenov // googleson78

e.g. one function could have an entirely different algorithm

Georgi Lyubenov // googleson78

so they're not really "the same" as "programs"

Georgi Lyubenov // googleson78

I'm not familiar with path equality, and don't know what it means there (and why you can use it with cubical)

Georgi Lyubenov // googleson78

I'm not sure about this, but if we want to be more precise, I'd wager that for two functions to be "the same" in vanilla agda (e.g. you can write refl : f == g) they need to have the same case/decision tree

Sam Toth

Ahh okay that makes sense. I guess for things to be able to be refl they need to have the same normal form - and since you cant pattern match/ deconstruct functions you can't build up any kind of proof to assert this. From a logical point of view I can see that just because two functions give the same result pointwise - to say that they are equal as a result is 'just like an opinion... man'

doing some testing in agda

  _+l_ :     
  zero +l b = b
  suc a +l b = suc (a +l b)

  _+r_ :     
  a +r zero = a
  a +r suc b = suc (a +r b)


  same : _+l_  _+r_
  same =  refl    -- does not type check

  _+l'_ :     
  zero +l' b = b
  suc a +l' b = suc (a +l' b)

  same2 : _+l_  _+l'_
  same2 =  refl    --  doesn't type check - but feels like it should

   id :  {A : Set}  A  A
  id = λ x  x

  id2 :  {A : Set}  A  A
  id2 = λ x  x

 -- Both of these type check

  test :  {A : Set}  id {A}  (λ x  x)
  test = refl

  test2 :  {A : Set}  id {A}  id2 {A}
  test2 = refl

I can understand why structurally +l and +r are distinct but it seems odd that test and test2 with id functions type check but the +l' and +l don't.

Sam Toth

Also from the book he says:

Postulating extensionality does not lead to difficulties, as it is known to be consistent with the theory that underlies Agda.

It would be interesting to understand why this is true but I'm sure I would need to understand much more type theory before I could handle that :confounded: