[Agda] 'finitely supported' constructively and without decidable equality

[Jacques Carette]

I am actually aware of these works [and have discussed them in person 
with Tarmo], along with The Coquand-Spiwak paper "Constructively 
Finite?".  The problem here is that 'finitely supported' turns out to be 
somewhat different in flavour than 'finite'.

In other words 'being finite' and describing a finite subset of 
something which isn't itself finite is quite different, constructively.  
In particular, trying to describe a finite subset of a type A which does 
not have a decidable equivalence relation seems tricky.

Twan's suggestion for FiniteSupport appears workable.  It looks like it 
gives enough information to let me sum f over all A (and obtain a finite 
result).  Which really is the crux of the matter.  Note that that 
definition of FiniteSupport has a good feature (shared with my use of 
Surjectivity): the 'support' only tells you where things are potentially 
not zero, and guarantees finiteness of that.  The uniqueness is nice to 
have, otherwise the proofs that the functor is actually adjoint gets 
really hard (one of the commutativity requirements and one of zig/zag, I 
don't remember which right now).

Jacques

PS: I should remark that Thorsten had privately sent me his suggestion 
(below) ~10 days ago (thanks!).  It did allow me to make some progress, 
but was still insufficient, because of the difference between 'finite' 
and 'finitely supported'.

On 2017-01-10 02:47 PM, Fredrik Nordvall Forsberg wrote:
> Dear Jacques,
>
> See also the work by Denis Firsov, Tarmo Uustalu, and Niccolo Veltri
> for comparisons between different encodings of finiteness in Agda,
> including Twan's and Thorsten's suggestions. (For instance, Twan's
> Finite A implies that A has decidable equality.)
>
> Denis Firsov and Tarmo Uustalu
> Dependently Typed Programming with Finite Sets
> WGP 2015
> http://dl.acm.org/authorize?N07761
>
> Denis Firsov, Tarmo Uustalu, and Niccolo Veltri
> Variations on Noetherianness
> MSFP 2016
> http://cs.ioc.ee/~tarmo/papers/msfp16b.pdf
>
> @inproceedings{firsov2015finiteSets,
>   author = {Firsov, Denis and Uustalu, Tarmo},
>   title = {Dependently Typed Programming with Finite Sets},
>   booktitle = {Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming},
>   pages = {33--44},
>   year = {2015},
>   publisher = {ACM},
> }
>
> @article{firsov2016variationsNoetherianness,
>    title={Variations on Noetherianness},
>    author={Firsov, Denis and Uustalu, Tarmo and Veltri, Niccolo},
>    journal={EPTCS},
>    volume={207},
>    pages={76--88},
>    year={2016},
>    publisher={Open Publishing Association}
> }
>
> Best wishes,
> Fred
>
> On 10/01/17 18:42, Thorsten Altenkirch wrote:
>> I think this is also equivalent to the definition I gave.
>>
>> data IsFin : Set → Set where
>> 	empty : IsFin ⊥
>> 	suc : ∀ {A} (a : A) → IsFin (A - a) → IsFin A
>>
>> If you want to avoid giving an ordering there is the following alternative:
>>
>>
>> data Noeth : Set → Set where
>> 	noeth : ∀ {A} → ((a : A) → Noeth (A - a)) → Noeth A
>>
>> Thorsten
>>
>>
>> P.S. Agda file attached.
>>
>>
>> On 10/01/2017, 18:21, twanvl at gmail.com wrote:
>>
>>> You could consider using a `List A` as a finite subset of A, so things
>>> like
>>>
>>>    record FiniteSupport {A : Set} (f : A → ℤ) where
>>>      field support : List A
>>>      field unsupported : ∀ {x} → x ∉ support → f x ≡ 0
>>>
>>> And finite sets would be:
>>>
>>>    record Finite (A : Set) where
>>>      field enum : List A
>>>      field member : ∀ x → x ∈ enum
>>>      -- optional:
>>>      field unique : ∀ {x} → (x∈enum : x ∈ enum) → x∈enum ≡ member x
>>>
>>> This is slightly stronger than just knowing that a type is finite, since
>>> you also get an ordering of the elements, but you also get this from a
>>> bijection with Fin.
>>>
>>> Twan
>>>
>>> On 2016-12-30 16:02, Jacques Carette wrote:
>>>> Given an arbitrary Set (type) A, is it possible to express that a type
>>>> such as "A → ℤ" is finitely supported?  The context is that of defining a free
>>>> abelian group, so I need to define a concept of Direct Sum.  I would prefer, if
>>>> at all possible, to make no assumptions on A.
>>>>
>>>> I have used
>>>>       B : Pred A o
>>>>       finite : Σ ℕ (λ n → (Σ A B ↣ Fin n))
>>>>
>>>> to define a "finitely supported subset of A" which 'works', but is
>>>> extremely awkward to work with.  In other places, I have seen people use the
>>>> existence of an induction principle as a proxy for finiteness [but they also assumed
>>>> a decidable equivalence on A].
>>>>
>>>> Jacques
>