Should Vec bundle like Signal?

[peter.t...@gmail.com]

I wanted transpose4:: Vec n (a,b,c,d) -> (Vec n a,Vec n b,Vec n c,Vec n d)

and thought to write

transpose4 = unbundle

(Yes, I know). Instead I had to write something quite nasty. A Vec is a short Signal, so perhaps it should bundle and  unbundle like one?

[ÉRDI Gergő]

On Sun, 7 Mar 2021, peter.t...@gmail.com wrote:

> I wanted transpose4:: Vec n (a,b,c,d) -> (Vec n a,Vec n b,Vec n c,Vec n d)
>
> and thought to write
>
> transpose4 = unbundle

Indeed, there's nothing special about `Signal` for bundling: being a
traversable applicative functor is enough. See details here:
https://github.com/clash-lang/clash-compiler/issues/1629

Unfortunately, changing `Bundle` along these lines leads to problems
basically because GHC has no generalized functional dependencies for
associated types, so we can't put `res f -> a` as a fundep...
https://github.com/clash-lang/clash-compiler/issues/1629#issuecomment-757833892

[peter.t...@gmail.com]

Isn't one saying that two functors, Vec n and tuple-ing, commute? (I suppose these are really functors in the category of categories, i.e., natural transformations, but I'm having sooooo much trouble with the  difference of nomeclatures between computer science and math).

That is:

class Bundle f g where

   bundle2 :: f (g x)(g y) -> g(f x y)

   unbundle2 :: g(f x y) -> f(g x)(g y)

   ...

instance KnownNat n => Bundle (Vec n) (,) where

   bundle2 (v1,v2) = zip2 v1 v2

   unbundle2 v = (map fst v, map snd v)

To go farther, I guess that you might want a property of tuples asserting the isomorphism of tuples of tuples with flattened tuples, which might be what you  call "traversable" (-ness  of  the pair constructor)?

I don't know where "applicative" would come in, because I have had a look at that definition, and it just seems to say "functor" (i.e., natural transformation ...) to me, plus an injection ("pure" - which I would 100% call "eta"!) to it from the identity functor (i.e., ...). It's always nice to have functors around, but the above definition doesn't use any functorial property ... yet. Perhaps one could get the higher order un/bundleN operations for free if one had some properties of f and g to rely on. By the time we've given ourselves enough properties that we're sat in a cartesian closed category, I would imagine yes one could.

Regards

Peter

[peter.t...@gmail.com]

What I meant was bundle3 (v1,(v2,v3)) = bundle((id .^^ bundle2) (v1,(v2,v3))) where (.^^) f g (x,y) = (f x,g y), so bundle3 = bundle2 . (id .^^ bundle2) .

And so on.

That works fine if (x,y,z)  is really (x,(y,z)) underneath, but perhaps in haskell/clash the tuple types are not represented internally like that, and then [and in any case] you will need the isomorphisms (x,y,z) <-> (x,(y,z)) to do a bit of before-and-afterwards fettling [even if the isomorphism is really just the identity valuewise, just ] to cast to and from the useful syntactic type.

I didn't understand the remarks on GitHub about the type family difficulty, because I don't know what = res->dom means (and not what a type family means .. maybe it's a parameterised type, maybe it's a constraint between types that has - or maybe has not - a many-one character). What's the difficulty with "Maybe", concretely?

Regards

Peter

[ÉRDI Gergő]

On Tue, 9 Mar 2021, peter.t...@gmail.com wrote:

> What I meant was bundle3 (v1,(v2,v3)) = bundle((id .^^ bundle2) (v1,(v2,v3))) where
> (.^^) f g (x,y) = (f x,g y), so bundle3 = bundle2 . (id .^^ bundle2) .
> And so on.

Your (.^^) is just (***) from Control.Arrow.

> I didn't understand the remarks on GitHub

Yeah, and that's OK. The discussion on the ticket is about implementation
strategies within the constraints of the typeclass system afforded by GHC.

[peter.t...@gmail.com]

> Your (.^^) is just (***) from Control.Arrow.

Yes. I don't seee that the Arrow class goes beyond categories, however. Perhaps it's meant to be an interface to categories without any mention of the application of a function to a value (i.e., just arrows and nothing else!). [And you should try searching for "***"!]

At least we all think the name should have three characters, and something to do with arrows!

And I really, really meant  (.^^) :: (x->u) -> (y->v) -> G x y -> G u v in full generality.

That is,  G  (i.e., "(,)") is the partner to the F (i.e. "Signal dom", or "Vec n") in a bundle/unbundle relationship between the two functors, with (.^^) f g p = pair(f(first p), g(second p)) and G x y is required to have pair :: x -> y -> G x y, first :: G x y -> x, second :: G x y -> y  with pair(first p,second p) = p and first(pair x y) = x, second(pair x y) = y.

The Arrow class seems to have what would make  isomorphisms between ((x,y),z) and (x,(y,z)) [and (x,y,z)?] possible. That is

assoc :: G x (G y z) -> G (G x y) z

with assoc  pair(pair x y) z = pair x (pair y z).

I would express that in arrows only ... but I have to sleep nights. I suppose it's not bad really.

But the point here is that it looks that one has enough leverage to generalise the bundle/unbundle stuff successfully, so what's the hitch expressed in GitHub? It seems to be  about not being sure which way to go with a bundle request when one has a Maybe mixed in there. I get that instances can sometimes overlap, causing confusion and mayhem, but perhaps a concrete example would help (me) see the problem?

Regards

Peter

[peter.t...@gmail.com]

Looking at Arrow class, I was interested by the associative property of pairs:

class Assoc f where
      assoc  :: f x (f y z) -> f (f x y) z
      assoc' :: f (f x y) z -> f x (f y z)
     

I was surprised that it suffices to have just curry and uncurry to get those, but it makes sense:

    ucurr :: (x -> y -> z) -> f x y -> z

    curr :: (f x y -> z) -> x -> y -> z

Then assoc and its inverse are expressible as:

 assoc  = ucurr(ucurr . curr (curr id))
 assoc' = ucurr(ucurr(curr . curr id))

(please take my word).  The big surprise is ... I have forgotten or I simply didn't know that curry and uncurry are all that is required, and everything else in a cartesian closed category can be expressed in terms of them. Here for example is the simple function pairing map (&&& of the Arrow category):

(&&&)  :: (x->y) -> (x->z) -> x -> f y z
 (&&&) f g x = curr id (f x) (g x)

That really is because curr id is the pairing operator itself, though nobody has said so. It just appeared!

curr id :: Assoc f => x -> y -> f x y

The projections out of pairs to the component parts also "just appear":

 

first :: f x y -> x
first = ucurr (\y _ -> y)

second :: f x y -> y
second = ucurr (\_ z -> z)

And so on. I haven't said that assoc and assoc' are mutual inverses, but if I did, I expect the semantic requirements for a CCC to be fulfilled throughout.

[One of the  ways of deriving the *** operation of the Arrow presentation is

(***)  :: (x->a) -> (y -> b) -> f x y -> f a b

 (***) f g = ucurr (\x _ -> f x) &&& ucurr (\_ y -> g y)

]

I guess the "type family" that was being talked about in the gitHub conversation was the sequence (,), (,,), (,,,), ... of n-tuples/ing. If so, that would make a type family mean something like a lot of type constructors with one more type parameter each time? And maybe one has defined (x,y,z,w) as really (x,(y,z,w)) underneath, plus a constructor name, like Pair4 x (y,z,w), to avoid confusions?

The point here is that if one defines a predicate Bundl indicating that functors f and g commute (which Is what bundling morally is - swapping two functors/constructors) and that bundl2 and unbundl2 are the isomorphism pair between the two equivalent representations, and I use the generalization of cartesian (closed) category [really a pre-category, since I have specified no semantics] above:

class Assoc f => Bundl g f where
      unbundl2 :: g(f x y) -> f(g x)(g y)
      bundl2   :: f(g x)(g y) -> g(f x y)

then one automatically gets the versions of bundling and unbundling for the (x,(y,z)) and (x,(y,(z,w))) and so on forms like this:

unbundl3 :: (Bundl g f)
          => g (f x (f y z)) -> f (g x) (f (g y) (g z))
unbundl3  = (id *** unbundl2) . unbundl2

The inverse is what one would expect  morally:

bundl3 :: (Bundl g f)
          => f (g x) (f (g y) (g z)) -> g (f x (f y z))
bundl3 = bundl2 . (id *** bundl2)

The rest of the sequence  is like this:

bundl4 = bundl3 . (id *** bundl3)
bundl5 = bundl4 . (id *** bundl4)

bundl6 = bundl5 . (id *** bundl5)

...

I presume the mysterious res->dom notation in type families is something like an inverse constructor, and maybe res stands for the codomain. If the binary type has been expanded to trinary via:

    f x y z = f x (f y z)

(and so on) then the above is saying

bundl3 :: f (g x) (g y) (g z) -> g (f x y z)

and one already has all the required bundling and unbundling ops. If there is a constructor thrown in underneath in order to avoid confusions, so one "really" has for example:

  f x y z = Pair4 x (f y z)

then one has to throw in some projections/retracts out of the Pair4 construction in order to get a suitable set of bundling/unbundling ops, and I still don't see the difficulty with overlapping instances ...

regards, comment welcome, etc.

[Christiaan Baaij]

The `res -> dom a` notation indicates injectivity of the type-level function. e.g. in

type family Unbundled (dom :: Domain) a = res | res -> dom a

we say that the result type of `Unbundle dom a` uniquely determines `dom` and `a`.

That means if I wrote the following two instances, GHC would reject them:

data Pair a b = MkPair a b

type instance Unbundled dom (a,b) = (Signal dom a, Signal dom b)

type instance Unbundled dom (Pair a b) = (Signal dom a, Signal dom b)

because the resulting type of the two instances `(Signal dom a, Signal dom b)` no longer uniquely determines the arguments.

We need this uniqueness/injectivity to get proper type inference.

However, when we define the type family as:

type family Unbundled (f :: Type -> Type) a = res | res -> f a

type instance Unbundled g (Vec n a) = Vec n (g a)

type instance Unbundled f (Maybe a) = f (Maybe a)

then those two instances overlap through the following unifications: g ~ Maybe; f ~ Vec n, and thus violate the injectivity.

And unlike class instances, type family instances are not allowed to overlap, not even with annotations.

Anyhow, that's why I started on a MultiParamTypeClasses + Functional Dependencies solution over at https://github.com/clash-lang/clash-compiler/pull/1699 that defines:

class Bundle f a res | f a -> res, a res -> f; f res -> a

where basically any triplet must be unique, thus aiding type inference.

We are however still allowed to overlap in case we want that for efficiency reasons (either Clash compile-time efficiency, or Clash simulation run-time efficiency):

instance {-# OVERLAPPABLE #-} (KnownNat n, Applicative f, Traversable f) => Bundle f (Vec n a) (Vec n (f a)) where
  bundle   = traverse# id
  unbundle = sequenceA . fmap lazyV

instance KnownNat n => Bundle (Signal dom) (Vec n a) (Vec n (Signal dom a)) where
  bundle   = vecBundle#
  unbundle = sequenceA . fmap lazyV

--
You received this message because you are subscribed to the Google Groups "Clash - Hardware Description Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to clash-languag...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/clash-language/554a12a9-20d4-49f6-8661-d20a9364407en%40googlegroups.com.

[peter.t...@gmail.com]

Thank you for that thoughtful post. Stuff inlined.

> type instance Unbundled dom (a,b) = (Signal dom a, Signal dom b)

I'll rephase/sumarise these things as I go, to make sure I have it right. The concept  there is that comma pairs of things can be rendered into  signals and the outcome  is essentially the same as a comma pair of signals. The mathematical idea in that is that SIgnal and comma pair commute as functors.

> type instance Unbundled dom (Pair a b) = (Signal dom a, Signal dom b)

Here the mathematical idea is not that Signal and Pair commute as functors, but that a signal containing Pairs is essentially the same as a comma pair of signals.

I would deduce from that, that comma pair and Pair are intrinsically isomorphic constructions, insofar as it may be deduced by an observer limited to think only in terms of signals, because of the polymorphic type arguments. [The qualification doesn't seem limiting in any way ... oh, what about signals of signals?  ]

I'd feel that the instance claim being made is programmatically dangerous because it entangles two concepts, and it should be that instead this weaker claim is put forward by the programmer:

 type instance Unbundled dom (Pair a b) = Pair (Signal dom a) (Signal dom b)

That  should state that Pair and Signal commute as functors. That would leave any further claim as to isomorphism between Pair and comma pair out of it for now,  at the further discretion of the programmer, if it were so desired.

> the resulting type of the two instances `(Signal dom a, Signal dom b)` no longer uniquely determines the arguments.

You are saying that you cannot determine if  you unbundled from a signal containing comma pairs, or a signal containing Pairs. But the rejection seems OK if one cares about that kind of thing, and one does care because one wants to be able to bundle back to the right type again, and there are now two alternatives.

However,  can one not disambiguate by specifying the (target) type  for bundle in each application? It's not going to be the only situation like that? It looks like an inconvenience rather than a problem.

You had

> type family Unbundled (dom :: Domain) a = res | res -> dom a

and now you will instead have

>  type family Unbundled (f :: Type -> Type) a = res | res -> f a

I'm not reading those "family" things well, though I understand (now/I think) from your explanation that the res -> foo stuff asserts one/ghc should be able to work out what the foo bar are that went into it when one sees an instance of Unbundled foo bar.

Checking: from the formal type of shape Signal dom (Pair a b) one could disentangle both dom and Pair a b. From Signal dom (a,b) one could disentangle both dom and (a,b).

Now you are claiming/will claim instead that from, say, a formal type of shape Signal dom x that has been proposed as a target type for unbundle, one can always figure out Signal dom and x.

> type instance Unbundled g (Vec n a) = Vec n (g a)

This will be a claim that applying unbundle to something  gets one a  Vec n (g a). But as things were, unbundle is supposed to apply to signals. Has unbundle now been respecified to apply now to things of form g, not Signal dom? Is it now

unbundle : : g(Vec n a) -> Vec n (g a)

Then g = Signal dom iwould be just one possibility for g, and g has generalized Signal dom.

> type instance Unbundled f (Maybe a) = f (Maybe a)

??? I am similarly to understand

unbundle :: f(Maybe a) -> f(Maybe a)

That doesn't seem to make sense as unbundle = id could always work for that. Was Maybe (f a) not f(Maybe a) was meant as the target type for unbundle? Perhaps this is a deliberate artifice ...

>  those two instances overlap through the following unifications: g ~ Maybe; f ~ Vec n, and thus violate the injectivity.

Yes, but isn't that saying one can't or shouldn't declare one of those two instances, hopefully the second, since it looked crazy to me (if I read these things right).

I can appreciate an intention here to artificially create an undesired solution via unification.  But if you had said in the standard context that

type instance Unbundled dom (Maybe a) = Signal dom (Maybe a)   -- !!

would you not also be creating difficulties, even if not quite the same sort? The problem looks to be that the example instance is mathematically wrong-headed whatever the context, and I would be happy to have it disallowed or otherwise screeched about by a compiler, so where's the problem?

If the intention is to show  definitions like

unbundle :: Bundled f g => f(g x y) -> g(f x)(f y)

bundle :: Bundled f g => g(f x)(f y) -> f(g x y)

give rise to ambiguities sometimes, that may be so and I do not necessarily have a problem with that.

But  ... provided one can see from  f foo what f  is and what foo is, and from g foo bar what g is and what foo is and what bar is, then one cannot mistake what bundle and unbundle are supposed to do in every situation. The type algorithm simply dismantles the argument type or the target type (and/or both simultaneously, via unifications) to get all of f, g, x, y in order to construct both the domain and codomain types for either of bundle or unbundle, as required. There is no ambiguity about it.

I think!

Peter

[peter.t...@gmail.com]

Reflecting, your perspective is that  Unbundled bar is an abbreviation for the domain type of bundle and the codomain type of unbundle.

The  problem may be that the unmentioned codomain/domain types are overspecified at present, and the abbreviation itself underspecified. The type of bundle "should" be Unbundled bar -> Bundled foo, and the type of unbundle should be Bundled foo -> Unbundled bar.

The codomain of bundle is currently Signal, which is also the domain of unbundle. Replace Signal dom with a new abbreviation Bundled foo. The  two abbreviations together will do the one binding I see, via unification and  type deconstructors.

That is   Unbundled f g x y = f (g x y)           -- c.f.: Signal dom (a,b)

               Bundled   f g x y    = g(f x)(f y)        -- c.f.: (Signal dom a,Signal dom b)

Do I understand the notation for that as  being:

type family Unbundled (f:: Type -> Type) (g :: Type -> Type -> Type) x y = res | f g x y

type family Bundled     (f :: Type -> Type) (g :: Type -> Type -> Type) x y = res | f g x y

?

The class declaration for Bundle introducing the methods bundle and unbundle should require both those abbreviations for the domains/codomains of the methods, and they are tied via unification in each instance of bundle and unbundle:

class Bundle f g where

   type family Unbundled ...

   type family Bundled ...

   bundle ::   Unbundled f g x y ->      Bundled f g x y

   unbundled :: Bundled f g x y -> Unbundled f g x y

Does that work? (modulo my guesses at syntax/what can be said)

Peter

[Christiaan Baaij]

The bundle type class was not created to transpose functors, but to distribute functions over product types (and to collect functors in the other direction).

So I don't think we need a `Bundled` type family, i.e. it's always:  Functor f => f ProductType.

wrt to your assertion that you should write:

type instance Unbundled dom (Pair a b) = Pair (Signal dom a) (Signal dom b)

you're absolutely correct. I was merely trying to demonstrate what the -XTypeFamilyDependencies extension prevents you from writing and why.

Finally, as to why we define things like:

type instance Unbundled dom (Maybe a) = Signal dom (Maybe a)

that's because we cannot write an information preserving version of:

instance Bundle dom (Maybe a) where

  type Unbundled dom (Maybe a) = Maybe (Signal dom a)

  bundle :: Maybe (Signal dom a) -> Signal dom (Maybe a)

  bundle Nothing = pure Nothing

  bundle (Just a) = Just <$> a

  unbundle :: Signal dom (Maybe a) -> Maybe (Signal dom a)

  unbundle = ???

because we cannot write an "unbundle" that preserves all information. So that's why we must write:

instance Bundle dom (Maybe a) where

  type Unbundled dom (Maybe a) = Signal dom (Maybe a)

  bundle :: Signal dom (Maybe a) -> Signal dom (Maybe a)

  bundle = id

  unbundle :: Signal dom (Maybe a) -> Signal dom (Maybe a)

  unbundle = id

if you wonder why we include that Bundle instance to begin with, it's so we only have to define a single variant of functions like `mealyB`:

mealyB :: (Bundle i, Bundle o) => (s -> i -> (s,o)) -> s -> (Unbundled dom i -> Unbundled dom o)

mealyB f start = unbundle . mealy f start . bundle

and it works regardless of whether both `i` and `o` are product types, or only one of `i` or `o` is a product type, since we define the Bundle instances for types that are _not_ products.

Again, the Bundle type class is about convenience.

To view this discussion on the web visit https://groups.google.com/d/msgid/clash-language/7c65e7a7-8f0d-4d61-943a-7f8bf4c27dbdn%40googlegroups.com.

[peter.t...@gmail.com]

> The bundle type class was not created to transpose functors, but to distribute functions over product types

That is the rationale, but it amounts to f (x,y) ~~ (f x,fy)  [where the symbol means something vague!] and that means that f applies to at least three different types, (x,y), x and y, which means it is a "family" of functions, which means it is part of a functor, not only a function. So it is about functors.

The  "equation"  is also about about the codomain types.  Your case is f = Signal dom, and Signal dom (x,y) ~~ (Signal dom x,Signal dom y). I thought you wanted isomorphism but I never went as far as writing that equation. I generalized pairs to some unspecified functor g, and Signal dom to some unspecified functor f, obtaining f (g x y) = g (f x) (f y), the  "=" being obtained by  declaring a pair of functors, bundle and unbundle.

To preserve your existing use of Bundled and Unbundled as the codomain (?) types of those two, rather than talk about some single class  that binds both f and g, I suggested  Bundled and Unbundled bind both f and g (aka SIgnal dom and (,)) , instead of just g (aka (,)) and through the unification that occurs in domains and codomains of  bundle and unbundle, figure out uniquely which f,g,x,y are meant in every concrete instance.

It's not different, just more general ...

You say you may want not isomorphism but  ... you say you want to bundle Maybe (Signal dom  x) to Signal dom (Maybe x). You point out  there is no inverse "unbundle" because bundle takes a small domain to a large domain and so must inevitably be a proper injection (or just function), so no (right) inverse can exist.

It's clearer if I use not Maybe x but Either x y [Maybe x is Either x ()]. You want to bundle Either (Signal dom x) (Signal dom y) to Signal dom (Either x y). Your bundle :: g (f x) (f y) -> f(g x y) is injective, i.e. information preserving.

You don't care about unbundle, so take something silly for it. Map to undefined :: Either (Signal dom x) (Signal dom y). It's the right type!

I would in general expect an adjunction, but I don't see that one has to require it if you are happy without.

Does that meet the objection? I.e., one can always define unbundle = const undefined if you really don't care about it, and hey, it's defined (as undefined). So requiring it to be defined does not hinder. Looks stubbornly unsynthesizable, but then other things are!

Regards

Peter