Jeremy Gibbons wrote:
I haven't assimilated the forall here, but datatypes with only one shape of data have been called "Naperian" by Peter Hancock (because they support a notion of logarithm), and they're instances of McBride and Paterson's "idioms" or "applicative functors".
http://sneezy.cs.nott.ac.uk/containers/blog/?p=14 http://www.cs.nott.ac.uk/~ctm/Idiom.pdf
As for uses: Bruno Oliveira and I claim an application via The Essence of the Iterator Pattern:
http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/index.html#iterator
Perhaps the key is that there exist types P and Q s.t. there's an isomorphism F a <=> (P -> a,Q) This seems to be intuitively Napierian: ln (P -> a,Q) = (P,ln a) | ln Q I can believe that Hoistables are in fact Idioms, though I know there are Idioms that are not Hoistables (Maybe and Either, for instance). (Also I think "Idiom" is a better class name than "Applicative".) -- Ashley Yakeley Seattle WA
I wrote:
Perhaps the key is that there exist types P and Q s.t. there's an isomorphism
F a <=> (P -> a,Q)
This seems to be intuitively Napierian:
ln (P -> a,Q) = (P,ln a) | ln Q
I can believe that Hoistables are in fact Idioms, though I know there are Idioms that are not Hoistables (Maybe and Either, for instance).
Ah, that's not correct, not all Hoistables are Idioms. For instance, this type can be made an instance of Hoistable but not of Idiom: data Extra a = MkExtra Int a -- Ashley Yakeley Seattle WA
participants (1)
-
Ashley Yakeley