Do you have to choose between composability and extra type safety?


Do you have to choose between composability and extra type safety?

As you know, I'm obsessed with the success of Haskell as a mainstream language. One thing that people out there need badly is composability.. I mean composability of libraries. Haskell can bring composability with mathematical soundness. The other thing needed that Haskell can bring is type safety.

But you have to choose between either extra type level guarantees or functional composability.

mathematically driven composability means the existence of seamless, algebraic operations (see link) of the kind

 A -> A -> A 

There may be many operations with this signature. for example: <>, <|>, + * or similar: <*>, <$> . >>=

Where A is a component which may include a number of effect and states to return something that will be combined with a second to produce a third while obeying some laws and so on.

The problem is that such kind of hard composability that allows seamless interoperability demand that both operands should have exactly the same types (or types very restricted in the case of <*> and >>=).

Suppose that you have two components. Imagine that they are made by different people or even different companies. then either the two have exactly the same types and that includes the same kind of states and effects -if you lift the state and effects to the type level- or you can not combine them with binary operators

This rule out monad transformers and free monads. extensible records etc as standards for the production of components.

And then the question:

Are there something in the Category Theory arsenal or in the Haskell ecosystem to overcome this?. I mean something with this signature:

 A(effs,states) a -> A(effs',states') a-> A(effs+effs',states+states´) a 

and also a kind of bind that accumulate states and effects, in order to combine components monadically:

A(effs,states) a-> (a -> (A(effs',states') b) -> A(effs+effs',states+states´) b 

Are there some operation such that this is implemented or at least it makes sense?

Submitted July 12, 2017 at 06:09PM by metafunctor
via reddit http://ift.tt/2ufdtux

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s