search

UniverseFly / Readings

Reading valuable research ideas while taking notes through GitHub Issues
0 stars 0 forks source link

Haskell'12 | Feat: functional enumeration of algebraic types #7

Closed UniverseFly closed 2 years ago

UniverseFly commented 2 years ago

https://www.cs.tufts.edu/~nr/cs257/archive/jonas-duregard/feat.pdf https://github.com/JonasDuregard/testing-feat

Besides FEAT, the author Dr. Duregard's successive works further elaborates the philosophy behind FEAT. And in this note I would explain its idea using the presentation of the first few sections of Generating Constrained Random Data with Uniform Distribution, which explains FEAT in a more understandable way with slightly-changed notations (e.g. the notion of function enumeration is replaced with a GADT Space, holding the same meaning, that can represent any ADT).

Also, please look into Dr. Duregard's Ph.D. thesis Automating Black-Box Property Based Testing which is an integration of all his works.

UniverseFly commented 2 years ago

Feat is a very very inspiring tool for generating/enumerating random structured data! I think it can serve as a foundation for other successive works.

UniverseFly commented 2 years ago

The idea is that each (maybe recursively defined) ADT (e.g. Nat, List, Bool) could be defined as a GADT Space (or a functional enumeration using the original notion from FEAT). Then all values of the ADT are partitioned w.r.t. their size, which could be roughly understood as #constructors applied. We have a sized function, defined on Space using pattern matching, to obtain one partition of some specific size. Finally we index the retrieved partition using an integer, which leads to the final result :).

I think this workflow is as easy as such thanks to the lazy evaluation of Haskell, which makes functions like sized and the infinite ADT defer its evaluation until we want the indexed value.

UniverseFly commented 2 years ago
image image image image
UniverseFly commented 2 years ago

The idea is that each (maybe recursively defined) ADT (e.g. Nat, List, Bool) could be defined as a GADT Space (or a functional enumeration using the original notion from FEAT). Then all values of the ADT are partitioned w.r.t. their size, which could be roughly understood as #constructors applied. We have a sized function, defined on Space using pattern matching, to obtain one partition of some specific size. Finally we index the retrieved partition using an integer, which leads to the final result :).

I think this workflow is as easy as such thanks to the lazy evaluation of Haskell, which makes functions like sized and the infinite ADT defer its evaluation until we want the indexed value.

In essense, as said in the paper, "Indexing on spaces can be reduced to two subproblems: Extracting the finite set of values of a particular set, and indexing into such finite sets".

For more details, look into the source code of FEAT.