Vague: Assembly line process

older
Re: Troubles Building LLVM (Fixed)

Martin Drautzburg

14 Jun 2010 14 Jun '10

1:16 p.m.

Hello all, this is a problem which has haunted me for some time. If this is simply hillarious, please tell me so. Or it may be some well known unsolvable problem... An assembly process takes inputs and produces outputs. I could say a Process is a function canProduce :: [Input]->[Output]->Bool which tells me if the outputs can be produced from the inputs There may be a similar function which tells me if the inputs are completely consumed to procude the output. The inputs do not determine the exact outputs. Think of a Process which combines a List of Ints into pairs, such that the input ints are consumed and each input Int occurs in only one position in the output. There are many ways to do this. Still for any set of input Ints and output pairs I could decide if the output can be produced from the input. Likewise the Input is not determined by the output. There may be lots of choices from what I could build my output (buy from different vendors). When I know more about the inputs and outputs my choices get more and more limited. I would like to to pass inputs and/or outputs to "something" and I would like to get a "something" which is more restricted, but still essentially a thing which tells me if the outputs can be produced from the inputs. I just cannot find a way to even THINK about this problem in a reasonable general way. -- Martin

Show replies by date

Luke Palmer

14 Jun 14 Jun

7:40 p.m.

So hang on, what is the problem? You have described something like a vague model, but what information are you trying to get? Say, perhaps, a set of possible output lists from a given input list? Luke On Mon, Jun 14, 2010 at 11:16 AM, Martin Drautzburg wrote:

...

Hello all,

this is a problem which has haunted me for some time. If this is simply hillarious, please tell me so. Or it may be some well known unsolvable problem...

An assembly process takes inputs and produces outputs. I could say a Process is a function

canProduce :: [Input]->[Output]->Bool

which tells me if the outputs can be produced from the inputs

There may be a similar function which tells me if the inputs are completely consumed to procude the output.

The inputs do not determine the exact outputs. Think of a Process which combines a List of Ints into pairs, such that the input ints are consumed and each input Int occurs in only one position in the output. There are many ways to do this. Still for any set of input Ints and output pairs I could decide if the output can be produced from the input.

Likewise the Input is not determined by the output. There may be lots of choices from what I could build my output (buy from different vendors).

When I know more about the inputs and outputs my choices get more and more limited. I would like to to pass inputs and/or outputs to "something" and I would like to get a "something" which is more restricted, but still essentially a thing which tells me if the outputs can be produced from the inputs.

I just cannot find a way to even THINK about this problem in a reasonable general way.

-- Martin _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Alexander Solla

10:24 p.m.

On Jun 14, 2010, at 4:40 PM, Luke Palmer wrote:

...

So hang on, what is the problem? You have described something like a vague model, but what information are you trying to get? Say, perhaps, a set of possible output lists from a given input list?

I think he's trying to construct a production possibility curve for a given set of inputs, and (probably) the most efficient production plan given the costs of his inputs. This is a problem I am going to have to solve programmatically, too. I intend on solving it by finding the input in a given category of necessary inputs with the lowest average cost per unit. I'm not concerned about "hard" cost allocation limits -- i.e. it's okay for the firm to buy more of an input than might be necessary for another output as long as the average unit cost is the lowest (since all the inputs will be used eventually anyway). Hard allocation complicates the problem, since you have an upper bound on what you can spend, and you want to spend it most effectively, presumably with as little "waste" of available cash as possibile. Bin packing. Martin: You need to find a nice "normal form" for inputs and outputs. If there aren't going to be many different types of inputs, you can deal with interchangeability by making a type for each type of input. (For example, if you were a jeweler, you could make:) type Price = Integer -- In cents, or a suitable denomination type Quantity = Integer data Mint = Perth | CreditSuisse | Sunshine | Kitco deriving (Eq, Show) data Gold = Gold Mint Quantity Price deriving (Eq, Show) data Silver = Silver Mint Quantity Price deriving (Eq, Show) class AverageCost commodity where average_cost_per_unit :: commodity -

...

Price instance (AverageCost commodity) => Ord commodity where -- I hope this isn't an undecidable instance left <= right = (average_cost_per_unit left) <= (average_cost_per_unit right)

data UnitOutput = UnitOutput { product :: Product, requires :: Requirement } data Requirement = Requirement { gold :: Gold, silver :: Silver } data Product = GoldWatch { style :: ... } | GoldChain { style :: ... } | SilverWatch { style :: ... } etc. How you encode the style/product/output relationship is up to you (maybe products should know their necessary inputs. Maybe not). If you have hard allocation limits, you can use a bin packing strategy.

Yitzchak Gale

16 Jun 16 Jun

5:16 a.m.

Alexander Solla wrote:

...

...and (probably) the most efficient production plan given the costs of his inputs. This is a problem I am going to have to solve programmatically, too. I intend on solving it by finding the input in a given category of necessary inputs with the lowest average cost per unit. I'm not concerned about "hard" cost allocation limits -- i.e. it's okay for the firm to buy more of an input than might be necessary for another output as long as the average unit cost is the lowest (since all the inputs will be used eventually anyway). Hard allocation complicates the problem, since you have an upper bound on what you can spend, and you want to spend it most effectively, presumably with as little "waste" of available cash as possibile. Bin packing.

This is Linear Programming: http://en.wikipedia.org/wiki/Linear_programming Regards, Yitz

Martin Drautzburg

15 Jun 15 Jun

1:23 p.m.

On Tuesday, 15. June 2010 01:40:03 Luke Palmer wrote:

...

So hang on, what is the problem? You have described something like a vague model, but what information are you trying to get? Say, perhaps, a set of possible output lists from a given input list?

When I know my supplies I want to know what I can produce. When I know what I want to produce I want to know what supplies I need for that. Both kinds of questions should be answered by a singe Process thingy. I want to be able to chain processes and the whole thing should still act like a Process.

...

Luke

On Mon, Jun 14, 2010 at 11:16 AM, Martin Drautzburg

wrote:

...
Hello all,

this is a problem which has haunted me for some time. If this is simply hillarious, please tell me so. Or it may be some well known unsolvable problem...

An assembly process takes inputs and produces outputs. I could say a Process is a function

canProduce :: [Input]->[Output]->Bool

which tells me if the outputs can be produced from the inputs

There may be a similar function which tells me if the inputs are completely consumed to procude the output.

The inputs do not determine the exact outputs. Think of a Process which combines a List of Ints into pairs, such that the input ints are consumed and each input Int occurs in only one position in the output. There are many ways to do this. Still for any set of input Ints and output pairs I could decide if the output can be produced from the input.

Likewise the Input is not determined by the output. There may be lots of choices from what I could build my output (buy from different vendors).

When I know more about the inputs and outputs my choices get more and more limited. I would like to to pass inputs and/or outputs to "something" and I would like to get a "something" which is more restricted, but still essentially a thing which tells me if the outputs can be produced from the inputs.

I just cannot find a way to even THINK about this problem in a reasonable general way.

-- Martin _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Martin

Steve Schafer

1:43 p.m.

On Tue, 15 Jun 2010 19:23:35 +0200, you wrote:

...

When I know my supplies I want to know what I can produce. When I know what I want to produce I want to know what supplies I need for that. Both kinds of questions should be answered by a singe Process thingy.

I want to be able to chain processes and the whole thing should still act like a Process.

This is a type of constraint network. If you have access to _Structure and Interpretation of Computer Programs_, there is a section therein devoted to constraint networks. See also: http://en.wikipedia.org/wiki/Constraint_programming Note that you need to be able to handle two kinds of "chaining": compoundContraint = constraint1 AND constraint2 -- the compound constraint isn't satisfied unless you can satisfy -- both primary constraints compoundContraint = constraint1 OR constraint2 -- the compound constraint is satisfied if either of the primary -- constraints is satisfied -Steve

Martin Drautzburg

16 Jun 16 Jun

12:30 p.m.

On Tuesday, 15. June 2010 19:43:26 Steve Schafer wrote:

...

On Tue, 15 Jun 2010 19:23:35 +0200, you wrote:

...
When I know my supplies I want to know what I can produce. When I know what I want to produce I want to know what supplies I need for that. Both kinds of questions should be answered by a singe Process thingy.

I want to be able to chain processes and the whole thing should still act like a Process.

This is a type of constraint network. If you have access to _Structure and Interpretation of Computer Programs_, there is a section therein devoted to constraint networks.

Will check this out. I was hoping that something simpler would suffice. I am afraid of CSPs. Today I was playing with a matrix representation. I mean the one you learn in school for linear optimization problems. Usually the matrix is written so it tells you how much of each supply you need to produce a unit of outputs. So when you know the outputs you can compute what you need as a minimum. You can invert the matrix and it'll work on the oppsite direction: when you know the inputs it'll tell you what you can produce at most. Then I thought, what if I replace the (*) and (+) operations which are applied when I multipy the matrix with a vector (i.e. a vector if inputs or outputs) by something more general. So I replaced (+) by function application and my matrix was now a matrix of functions. But then I got lost trying to find a way to invert such a matrix. FWIW: while googeling around how to invert a matrix of functions I stumbeled across the "Process Specification Language". At least they defined an ontology, but there isn't much of computing stuff there. http://www.mel.nist.gov/psl/ -- Martin

Steve Schafer

1:18 p.m.

On Wed, 16 Jun 2010 18:30:47 +0200, you wrote:

...

Then I thought, what if I replace the (*) and (+) operations which are applied when I multipy the matrix with a vector (i.e. a vector if inputs or outputs) by something more general. So I replaced (+) by function application and my matrix was now a matrix of functions. But then I got lost trying to find a way to invert such a matrix.

You'd have to have a general way of finding the inverse of a function, which doesn't exist (many functions aren't invertible at all, for example). -Steve

Bas van Dijk

15 Jun 15 Jun

3:26 p.m.

On Tue, Jun 15, 2010 at 7:23 PM, Martin Drautzburg wrote:

...

When I know my supplies I want to know what I can produce. When I know what I want to produce I want to know what supplies I need for that. Both kinds of questions should be answered by a singe Process thingy.

Your Process thingy reminds me of a natural isomorphism: data Iso a b = Iso { ab :: a -> b , ba :: b -> a }

...

I want to be able to chain processes and the whole thing should still act like a Process.

These isomorphisms can be chained together using the standard Category method '.': import qualified Control.Category as C instance C.Category Iso where id = Iso id id Iso bc cb . Iso ab ba = Iso (bc . ab) (ba . cb)

Bas van Dijk

16 Jun 16 Jun

3:36 a.m.

On Tue, Jun 15, 2010 at 9:26 PM, Bas van Dijk wrote:

...

On Tue, Jun 15, 2010 at 7:23 PM, Martin Drautzburg wrote:

...
When I know my supplies I want to know what I can produce. When I know what I want to produce I want to know what supplies I need for that. Both kinds of questions should be answered by a singe Process thingy.

Your Process thingy reminds me of a natural isomorphism:

data Iso a b = Iso { ab :: a -> b , ba :: b -> a }

...
I want to be able to chain processes and the whole thing should still act like a Process.

These isomorphisms can be chained together using the standard Category method '.':

import qualified Control.Category as C

instance C.Category Iso where id = Iso id id Iso bc cb . Iso ab ba = Iso (bc . ab) (ba . cb)

I couldn't help to generalize this a bit: -# LANGUAGE TypeOperators, UnicodeSyntax #-} import Control.Category import Control.Arrow import Prelude hiding (id, (.)) data Iso (⇝) a b = Iso { ab ∷ a ⇝ b , ba ∷ b ⇝ a } type IsoFunc = Iso (→) instance Category (⇝) ⇒ Category (Iso (⇝)) where id = Iso id id Iso bc cb . Iso ab ba = Iso (bc . ab) (ba . cb) An 'Iso (⇝)' also _almost_ forms an Arrow (if (⇝) forms an Arrow): instance Arrow (⇝) ⇒ Arrow (Iso (⇝)) where arr f = Iso (arr f) undefined first (Iso ab ba) = Iso (first ab) (first ba) second (Iso ab ba) = Iso (second ab) (second ba) Iso ab ba *** Iso cd dc = Iso (ab *** cd) (ba *** dc) Iso ab ba &&& Iso ac ca = Iso (ab &&& ac) (ba . arr fst) -- or: (ca . arr snd) But note the unfortunate 'undefined' in the definition of 'arr'. This seems to suggest that all the methods besides 'arr' need to move to a separate type class. Maybe something like: class Category (⇝) ⇒ Arrow (⇝) where arr ∷ (a → b) → (a ⇝ b) class Category (⇝) ⇒ Pass (⇝) where first ∷ (a ⇝ b) → ((a, c) ⇝ (b, c)) second ∷ (a ⇝ b) → ((c, a) ⇝ (c, b)) (***) ∷ (a ⇝ b) → (c ⇝ d) → ((a, c) ⇝ (b, d)) (&&&) ∷ (a ⇝ b) → (a ⇝ c) → (a ⇝ (b, c)) Oh well... Bas

Tillmann Rendel

6:55 a.m.

New subject: The Arrow class (was: Vague: Assembly line process)

Bas van Dijk wrote:

...

data Iso (⇝) a b = Iso { ab ∷ a ⇝ b , ba ∷ b ⇝ a }

type IsoFunc = Iso (→)

instance Category (⇝) ⇒ Category (Iso (⇝)) where id = Iso id id Iso bc cb . Iso ab ba = Iso (bc . ab) (ba . cb)

An 'Iso (⇝)' also _almost_ forms an Arrow (if (⇝) forms an Arrow):

instance Arrow (⇝) ⇒ Arrow (Iso (⇝)) where arr f = Iso (arr f) undefined

first (Iso ab ba) = Iso (first ab) (first ba) second (Iso ab ba) = Iso (second ab) (second ba) Iso ab ba *** Iso cd dc = Iso (ab *** cd) (ba *** dc) Iso ab ba &&& Iso ac ca = Iso (ab &&& ac) (ba . arr fst) -- or: (ca . arr snd)

But note the unfortunate 'undefined' in the definition of 'arr'.

This seems to suggest that all the methods besides 'arr' need to move to a separate type class.

I agree. The power of Arrows as they currently are is that we can enlarge the ordinary set of functions (->). But if arr would be excluded from the Arrow class, we could remove arrows, too. For example, in your Iso example, we want to consider not all morphisms, but only the isomorphisms. It would be nice to have a standard type class to express this kind of thing, and it would be nice to have arrow notation (or some variant of arrow notation) for it. However, I'm not so sure about the types of (***) etc. Currently, we have (***) :: (a ~> b) -> (c ~> d) -> ((a, c) ~> (b, d)) (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> (b, c)) This seems to say that (~>) has products as follows: The object part of the product bifunctor is (,), the morphism part of the product bifunctor is (***), the mediating arrow is constructed by (&&&), and the projections are (arr fst) and (arr snd). I see two problems with this definition: The object part of the bifunctor is fixed, and the projections are given in terms of arr. Wouldn't it be better to have a definition like this: class Category (~>) => Products (~>) where (***) :: (a ~> b) -> (c ~> d) -> ((a, c) ~> (b, d)) (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> (b, c)) fst :: (a, b) ~> a snd :: (a, b) ~> b Or even like this: class Category (~>) => Products (~>) where type Product a b (***) :: (a ~> b) -> (c ~> d) -> (Product a c ~> Product b d) (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> Product b c) fst :: Product a b ~> a snd :: Product a b ~> b Unfortunately, I don't see how to define fst and snd for the Iso example, so I wonder whether Iso has products? Tillmann

Edward Kmett

2:18 p.m.

New subject: The Arrow class (was: Vague: Assembly line process)

On Wed, Jun 16, 2010 at 6:55 AM, Tillmann Rendel < rendel@mathematik.uni-marburg.de> wrote:

...

Bas van Dijk wrote:

...
data Iso (⇝) a b = Iso { ab ∷ a ⇝ b , ba ∷ b ⇝ a }

type IsoFunc = Iso (→)

instance Category (⇝) ⇒ Category (Iso (⇝)) where id = Iso id id Iso bc cb . Iso ab ba = Iso (bc . ab) (ba . cb)

An 'Iso (⇝)' also _almost_ forms an Arrow (if (⇝) forms an Arrow):

instance Arrow (⇝) ⇒ Arrow (Iso (⇝)) where arr f = Iso (arr f) undefined

first (Iso ab ba) = Iso (first ab) (first ba) second (Iso ab ba) = Iso (second ab) (second ba) Iso ab ba *** Iso cd dc = Iso (ab *** cd) (ba *** dc) Iso ab ba &&& Iso ac ca = Iso (ab &&& ac) (ba . arr fst) -- or: (ca . arr snd)

But note the unfortunate 'undefined' in the definition of 'arr'.

This comes up every couple of years, I think the first attempt at formulating Iso wrongly as an arrow was in the "There and Back Again" paper. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.7278 It comes up now and again, because the types seem to _almost_ fit. =) The reason is that an arrow is a closed pre-Cartesian category with a little bit of extra structure. Isomorphisms and embedding-projection pairs are a bit too constrained to meet even the requirements of a pre-Cartesian category, however. This seems to suggest that all the methods besides 'arr' need to move

...

...
to a separate type class.

You may be interesting in following the construction of a more formal set of categories that build up the functionality of arrow incrementally in category-extras. An arrow can be viewed as a closed pre-cartesian category with an embedding of Hask. Iso on the other hand is much weaker. The category is isomorphisms, or slightly weaker, the category of embedding-projection pairs doesn't have all the properties you might expect at first glance. You an define it as a Symmetric Monoidal category over (,) using a Bifunctor for (,) over Iso: http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/... the assocative laws from: http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/... The definitions of Braided and Symmetric from: http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/... and the Monoidal class from: http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/... This gives you a weak product-like construction. But as you noted, fst and snd cannot be defined, so you cannot define Cartesian http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/... let alone a CCC http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/... or Arrow. =( Wouldn't it be better to have a definition like this:

...

class Category (~>) => Products (~>) where (***) :: (a ~> b) -> (c ~> d) -> ((a, c) ~> (b, d)) (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> (b, c)) fst :: (a, b) ~> a snd :: (a, b) ~> b

You've stumbled across the concept of a Cartesian category (or at least, technically 'pre-Cartesian', though the type of product also needs to be a parameter or the dual of a category with sums won't be a category with products. http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/... Or even like this:

...

class Category (~>) => Products (~>) where type Product a b (***) :: (a ~> b) -> (c ~> d) -> (Product a c ~> Product b d) (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> Product b c) fst :: Product a b ~> a snd :: Product a b ~> b

This was the formulation I had originally used in category-extras for categories. I swapped to MPTCs due to implementation defects in type families at the time, and intend to swap back at some point in the future.

...

Unfortunately, I don't see how to define fst and snd for the Iso example, so I wonder whether Iso has products?

It does not. =) -Edward Kmett

Ryan Ingram

18 Jun 18 Jun

7:57 p.m.

New subject: The Arrow class (was: Vague: Assembly line process)

Related to this, I really would like to be able to use arrow notation without "arr"; I was looking into writing a "circuit optimizer" that modified my arrow-like circuit structure, but since it's impossible to "look inside" arr, I ran into a brick wall. Has anyone done any analysis of what operations arrow notation actually requires so that they can be made methods of some typeclass, instead of defining everything in terms of "arr"? It seems to me the trickiness comes when you have patterns and complex expressions in your arrow notation, that is, you write (a,b) <- some_arrow <- (c,d) returnA -< a instead of x <- some_arrow <- y returnA -< x But I expect to be able to do the latter without requiring "arr", and that does not seem to happen. -- ryan On Wed, Jun 16, 2010 at 11:18 AM, Edward Kmett wrote:

...

On Wed, Jun 16, 2010 at 6:55 AM, Tillmann Rendel wrote:

...
Bas van Dijk wrote:

...
data Iso (⇝) a b = Iso { ab ∷ a ⇝ b , ba ∷ b ⇝ a }

type IsoFunc = Iso (→)

instance Category (⇝) ⇒ Category (Iso (⇝)) where id = Iso id id Iso bc cb . Iso ab ba = Iso (bc . ab) (ba . cb)

An 'Iso (⇝)' also _almost_ forms an Arrow (if (⇝) forms an Arrow):

instance Arrow (⇝) ⇒ Arrow (Iso (⇝)) where arr f = Iso (arr f) undefined

first (Iso ab ba) = Iso (first ab) (first ba) second (Iso ab ba) = Iso (second ab) (second ba) Iso ab ba *** Iso cd dc = Iso (ab *** cd) (ba *** dc) Iso ab ba &&& Iso ac ca = Iso (ab &&& ac) (ba . arr fst) -- or: (ca . arr snd)

But note the unfortunate 'undefined' in the definition of 'arr'.

This comes up every couple of years, I think the first attempt at formulating Iso wrongly as an arrow was in the "There and Back Again" paper.

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.7278

It comes up now and again, because the types seem to _almost_ fit. =) The reason is that an arrow is a closed pre-Cartesian category with a little bit of extra structure. Isomorphisms and embedding-projection pairs are a bit too constrained to meet even the requirements of a pre-Cartesian category, however.

...
...
This seems to suggest that all the methods besides 'arr' need to move to a separate type class.

You may be interesting in following the construction of a more formal set of categories that build up the functionality of arrow incrementally in category-extras. An arrow can be viewed as a closed pre-cartesian category with an embedding of Hask. Iso on the other hand is much weaker. The category is isomorphisms, or slightly weaker, the category of embedding-projection pairs doesn't have all the properties you might expect at first glance.

You an define it as a Symmetric Monoidal category over (,) using a Bifunctor for (,) over Iso:

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/...

the assocative laws from:

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/...

The definitions of Braided and Symmetric from:

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/...

and the Monoidal class from:

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/...

This gives you a weak product-like construction. But as you noted, fst and snd cannot be defined, so you cannot define Cartesian

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/...

let alone a CCC

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/...

or Arrow. =(

...
Wouldn't it be better to have a definition like this:

class Category (~>) => Products (~>) where (***) :: (a ~> b) -> (c ~> d) -> ((a, c) ~> (b, d)) (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> (b, c)) fst :: (a, b) ~> a snd :: (a, b) ~> b

You've stumbled across the concept of a Cartesian category (or at least, technically 'pre-Cartesian', though the type of product also needs to be a parameter or the dual of a category with sums won't be a category with products.

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/...

...
Or even like this:

class Category (~>) => Products (~>) where type Product a b (***) :: (a ~> b) -> (c ~> d) -> (Product a c ~> Product b d) (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> Product b c) fst :: Product a b ~> a snd :: Product a b ~> b

This was the formulation I had originally used in category-extras for categories. I swapped to MPTCs due to implementation defects in type families at the time, and intend to swap back at some point in the future.

...
Unfortunately, I don't see how to define fst and snd for the Iso example, so I wonder whether Iso has products?

It does not. =)

-Edward Kmett

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Edward Kmett

10:38 p.m.

New subject: The Arrow class (was: Vague: Assembly line process)

Hi Ryan, On Fri, Jun 18, 2010 at 7:57 PM, Ryan Ingram wrote:

...

Related to this, I really would like to be able to use arrow notation without "arr"; I was looking into writing a "circuit optimizer" that modified my arrow-like circuit structure, but since it's impossible to "look inside" arr, I ran into a brick wall.

Has anyone done any analysis of what operations arrow notation actually requires so that they can be made methods of some typeclass, instead of defining everything in terms of "arr"?

It seems to me the trickiness comes when you have patterns and complex expressions in your arrow notation, that is, you write

(a,b) <- some_arrow <- (c,d) returnA -< a

The design I've been using for this has been to use data-reify, and observable sharing and to use pure let bindings to build the circuit. full_adder :: Bit -> Bit -> Bit -> (Bit, Bit) full_adder a b cin = (s2, c1 || c2) where (s1,c1) = half_adder a b (s2,c2) = half_adder s1 cin half_adder :: Bit -> Bit -> (Bit, Bit) half_adder a b = (a `xor` b, a && b) foo = do x <- exists y <- exists z <- exists assert $ full_adder x y z === (1,1) assert $ forall $ \ a b c -> (a && b) ==> c === (a ==> b ==> c) return (x,y,z) I perform a similar sharing recovery in the back end code of Numeric.RAD from the 'rad' package and Numeric.AD.Internal.Reverse in the 'ad' package. I have uses in a number of unreleased bottom-up applicative parser combinators as well, so it has a wide arrange of applicable situations. Overall, let bindings tend to be a lot lighter than the accompanying arrow sugar. You might find Andy Gill's write-up on type safe observable sharing in kansas lava to be useful. http://www.ittc.ku.edu/~andygill/papers/reifyGraph.pdf -Edward Kmett

Luke Palmer

19 Jun 19 Jun

4:20 p.m.

New subject: The Arrow class (was: Vague: Assembly line process)

On Fri, Jun 18, 2010 at 5:57 PM, Ryan Ingram wrote:

...

Related to this, I really would like to be able to use arrow notation without "arr"; I was looking into writing a "circuit optimizer" that modified my arrow-like circuit structure, but since it's impossible to "look inside" arr, I ran into a brick wall.

Has anyone done any analysis of what operations arrow notation actually requires so that they can be made methods of some typeclass, instead of defining everything in terms of "arr"?

Well, there's DeepArrow. I'm not sure if it's minimal or anything, but IIRC that was its purpose.

...

It seems to me the trickiness comes when you have patterns and complex expressions in your arrow notation, that is, you write

(a,b) <- some_arrow <- (c,d) returnA -< a

instead of

x <- some_arrow <- y returnA -< x

But I expect to be able to do the latter without requiring "arr", and that does not seem to happen.

-- ryan

On Wed, Jun 16, 2010 at 11:18 AM, Edward Kmett wrote:

...
On Wed, Jun 16, 2010 at 6:55 AM, Tillmann Rendel wrote:

...
Bas van Dijk wrote:

...
data Iso (⇝) a b = Iso { ab ∷ a ⇝ b , ba ∷ b ⇝ a }

type IsoFunc = Iso (→)

instance Category (⇝) ⇒ Category (Iso (⇝)) where id = Iso id id Iso bc cb . Iso ab ba = Iso (bc . ab) (ba . cb)

An 'Iso (⇝)' also _almost_ forms an Arrow (if (⇝) forms an Arrow):

instance Arrow (⇝) ⇒ Arrow (Iso (⇝)) where arr f = Iso (arr f) undefined

first (Iso ab ba) = Iso (first ab) (first ba) second (Iso ab ba) = Iso (second ab) (second ba) Iso ab ba *** Iso cd dc = Iso (ab *** cd) (ba *** dc) Iso ab ba &&& Iso ac ca = Iso (ab &&& ac) (ba . arr fst) -- or: (ca . arr snd)

But note the unfortunate 'undefined' in the definition of 'arr'.

This comes up every couple of years, I think the first attempt at formulating Iso wrongly as an arrow was in the "There and Back Again" paper.

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.7278

It comes up now and again, because the types seem to _almost_ fit. =) The reason is that an arrow is a closed pre-Cartesian category with a little bit of extra structure. Isomorphisms and embedding-projection pairs are a bit too constrained to meet even the requirements of a pre-Cartesian category, however.

...
...
This seems to suggest that all the methods besides 'arr' need to move to a separate type class.

You may be interesting in following the construction of a more formal set of categories that build up the functionality of arrow incrementally in category-extras. An arrow can be viewed as a closed pre-cartesian category with an embedding of Hask. Iso on the other hand is much weaker. The category is isomorphisms, or slightly weaker, the category of embedding-projection pairs doesn't have all the properties you might expect at first glance.

You an define it as a Symmetric Monoidal category over (,) using a Bifunctor for (,) over Iso:

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/...

the assocative laws from:

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/...

The definitions of Braided and Symmetric from:

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/...

and the Monoidal class from:

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/...

This gives you a weak product-like construction. But as you noted, fst and snd cannot be defined, so you cannot define Cartesian

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/...

let alone a CCC

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/...

or Arrow. =(

...
Wouldn't it be better to have a definition like this:

class Category (~>) => Products (~>) where (***) :: (a ~> b) -> (c ~> d) -> ((a, c) ~> (b, d)) (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> (b, c)) fst :: (a, b) ~> a snd :: (a, b) ~> b

You've stumbled across the concept of a Cartesian category (or at least, technically 'pre-Cartesian', though the type of product also needs to be a parameter or the dual of a category with sums won't be a category with products.

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/...

...
Or even like this:

class Category (~>) => Products (~>) where type Product a b (***) :: (a ~> b) -> (c ~> d) -> (Product a c ~> Product b d) (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> Product b c) fst :: Product a b ~> a snd :: Product a b ~> b

This was the formulation I had originally used in category-extras for categories. I swapped to MPTCs due to implementation defects in type families at the time, and intend to swap back at some point in the future.

...
Unfortunately, I don't see how to define fst and snd for the Iso example, so I wonder whether Iso has products?

It does not. =)

-Edward Kmett

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

5451

Age (days ago)

5456

Last active (days ago)

List overview

Download

14 comments

9 participants

participants (9)

Alexander Solla
Bas van Dijk
Edward Kmett
Luke Palmer
Martin Drautzburg
Ryan Ingram
Steve Schafer
Tillmann Rendel
Yitzchak Gale