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

[Fredrik Nordvall Forsberg]

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


-- 
Fredrik Nordvall Forsberg,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.