質問

In a library I'm writing I've found it to be seemingly elegant to write a class that is similar to (but slightly more general than) the following, which combines both the usual uncurry over products and the fanin function (from here, or here if you prefer):

{-# LANGUAGE TypeOperators, TypeFamilies,MultiParamTypeClasses, FlexibleInstances #-}
import Prelude hiding(uncurry)
import qualified Prelude 

class Uncurry t r where
    type t :->-> r
    uncurry :: (t :->-> r) -> t -> r

instance Uncurry () r where
    type () :->-> r = r
    uncurry = const

instance Uncurry (a,b) r where
    type (a,b) :->-> r = a -> b -> r
    uncurry = Prelude.uncurry

instance (Uncurry b c, Uncurry a c)=> Uncurry (Either a b) c where
    type Either a b :->-> c = (a :->-> c, b :->-> c)
    uncurry (f,g) = either (uncurry f) (uncurry g)

I usually browse Edward Kmett's categories package (linked above) to get my bearings for this sort of thing, but in that package we have fanin and uncurry separated into the CoCartesian and CCC classes respectively.

I've read a bit about BiCCCs but don't really understand them yet.

My questions are

  1. Is the abstraction above justified by some way of squinting at category theory?

  2. If so what would be the proper CT-grounded language to talk about the class and its instances?


EDIT: In case it helps and the simplification above is distorting things: in my actual application I'm working with nested products and coproducts, e.g. (1,(2,(3,()))). Here is the real code (although for boring reasons the last instance is simplified, and doesn't work alone as written)

instance Uncurry () r where
    type () :->-> r = r
    uncurry = const

instance (Uncurry bs r)=> Uncurry (a,bs) r where
    type (a,bs) :->-> r = a -> bs :->-> r
    uncurry f = Prelude.uncurry (uncurry . f)

-- Not quite correct
instance (Uncurry bs c, Uncurry a c)=> Uncurry (Either a bs) c where
    type Either a bs :->-> c = (a :->-> c, bs :->-> c)
    uncurry (f,fs) = either (uncurry f) (uncurry fs) -- or as Sassa NF points out:
                                                     -- uncurry (|||)

So the const instance for () instance came naturally as the recursive base case for the n-ary tuple uncurry instance, but seeing all three together looked like... something non-arbitrary.


Update

I found that thinking in terms of algebraic operations, a.la Chris Taylor's blogs about the "algebra of ADTs". Doing so clarified that my class and methods were really just the exponent laws (and the reason why my last instance was not right).

You can see the result in my shapely-data package, in the Exponent and Base classes; see also the source for notes and non-wonky doc markup.

役に立ちましたか?

解決

Your last Uncurry instance is exactly the uncurry (|||), so there is nothing "more general" about it.

Curry finds for any arrow f: A×B→C an arrow curryf: A→CB such that a unique arrow eval: CB×B→C commutes. You can view eval as ($). Saying "CCC" is the shorthand for "in this category we have all products, all exponents, and a terminal object" - in other words, currying works for any pair of types and any function in haskell. One important consequence of being a CCC is that A=1×A=A×1 (or a is isomorphic to (a,()) and isomorphic to ((),a)).

Uncurry in haskell is the opposite labelling of the same process. We start with an arrow f=uncurryg. Each pair has two projections, so a composition of proj1 and curryf=g gives a CB. Since we are talking about composition and products, uncurrying in CCC defines a unique uncurryg for any g: A→CB. In CCC we have all products, so we have CB×B, which can be evaled to C.

In particular, recall A=A×1. This means that any function A→B is also a function A×1→B. You could also view this as "for any function A→B there is a function A×1→B" proven by trivial uncurrying, of which your first instance does only a half (only proves this for id).

I wouldn't call the last instance a "uncurry" in the same sense as currying is defined. The last instance is a construction of the definition of co-product - for any pair of arrows f: A→C and g: B→C there is a unique arrow [f,g]: (A+B)→C. In this sense it seems as abuse of the interface - it is a generalization of meaning from "uncurry" to "given something, give me something" or "a true correspondence between :->-> and haskell functions". Perhaps, you could rename the class to Arrow.

ライセンス: CC-BY-SA帰属
所属していません StackOverflow
scroll top