fantasyland / fantasy-land

Specification for interoperability of common algebraic structures in JavaScript
MIT License
10.12k stars 374 forks source link

Proposal: specs for Maybe, Either, Tuple, Task, ... #185

Open gcanti opened 8 years ago

gcanti commented 8 years ago

Sorry if it was discussed before, after scanning the issues I didn't find anything on the subject.

The motivation comes from the last addition: the spec for chainRec which I find hard to understand

chainRec :: ChainRec m => ((a -> c, b -> c, a) -> m c, a) -> m b

with respect to

class Monad m <= MonadRec m where
  tailRecM :: forall a b. (a -> m (Either a b)) -> a -> m b

Relevant issues

I understand the benefits of not depending on a particular implementation of Either but why fantasy-land doesn't provide a spec for Either in the first place?

For example writing the spec for Unfoldable would be problematic (Maybe AND Tuple)

class Unfoldable t where
  unfoldr :: forall a b. (b -> Maybe (Tuple a b)) -> b -> t a

We have great libraries out there for Maybe, Either, Task, etc... but there's no standard for them.

Would it be a good idea to add specs for these concrete types?

rpominov commented 8 years ago

Just as another example: a spec for Maybe could be used for mapMaybe https://github.com/fantasyland/fantasy-land/issues/33#issuecomment-222539961

SimonRichardson commented 8 years ago

Having used chainRec a few times now, I wish we had used Either.

I'm not totally sold on a whole spec for either as they type should say enough?

safareli commented 8 years ago

You can use Either and before returning it just do .fold(next, done) on it

About unfoldr it's type could be:

// unfoldr :: (Unfoldable t) => (((a, b) -> c, c, b) -> c) -> b -> t a
List.unfoldr((next, done, x) => x > 100 ? done : next(x*x, x+1), 0)

Also for example sanctuary or folktale could on their own Either and expose this function:

// chainRecWithEither :: (ChainRec m) => (TypRep m, a -> m (Either a r), a) -> m r
const chainRecWithEither = (T,f,i) => T.chainRec(
  (next,done,x) => f(x).map(e => e.fold(next,done)),
  i
)

Also using Either in chainRec is not a quite good idea imo. For example recently I saw there is an elm module elm-tail-recursion which uses Left as done and Right as next, when in old version of purescript-tailrec Left was used as next and Right as done. In current version of purescript-tailrec we have data Step a b = Loop a | Done b which I think better than Either.

SimonRichardson commented 8 years ago

Thanks @safareli some food for thought :+1:

rpominov commented 8 years ago

Good point about ambiguous meaning of Left and Right in chainRec. Maybe we could have some general spec that would describe APIs of sum and product types? Something like a spec for daggy's cata method.

safareli commented 8 years ago

general spec that would describe APIs of sum and product types @rpominov that's much better idea!

Some sketch of ideas:

// Step a b = Loop a | Done b
Step.types = ['Loop', 'Done']
Step.Loop = (a)  => ({ 
  type: Step.types[0], 
  constructor: Step,
  values: { _1: a },
  keys: ['_1'],
})
Step.Done = (a)  => ({ 
  type: Step.types[1], 
  constructor: Step,
  values: { _1: a },
  keys: ['_1'],
})

// Maybe a = Nothing | Just a
Maybe.types = ['Nothing', 'Just']
Maybe.Just = (a)  => ({ 
  type: Maybe.types[1], 
  constructor: Maybe,
  values: { _1: a },
  keys: ['_1'],
})
Maybe.Nothing = { 
  type: Maybe.types[0]
  constructor: Maybe,
  values: {},
  keys: [],
}

// List a = Nil | Cons a (List a)
List.types = ['Nil', 'Cons']
List.Cons = (a, b)  => ({ 
  type: List.types[1], 
  constructor: List,
  values: { _1: a, _2: b },
  keys: ['_1', '_2'],
})
List.Nil = { 
  type: List.types[0],
  constructor: List,
  values: {},
  keys: [],
}

// Tree a = Empty | Leaf a | Node a (Tree a) (Tree a)
Tree.types = ['Empty', 'Leaf', 'Node']
Tree.Node = (a, b, c)  => ({ 
  type: Tree.types[2], 
  constructor: Tree,
  values: { _1: a, _2: b , _3: c },
  keys: ['_1', '_2', '_3'],
})
Tree.Leaf = (a) => ({ 
  type: Tree.types[1], 
  constructor: Tree,
  values: { _1: a },
  keys: ['_1'],
})
Tree.Empty = { 
  type: Tree.types[0],
  constructor: Tree,
  values: {},
  keys: [],
}

using type, keys and values we can implement general fold or cata:

const valuesAsArray = v => {
  let args = []
  for (var i = 0; i < v.keys.length; i++) {
    args.push(v.values[v.keys[i]])  
  }
  return args
}
const fold = (fs, v) => {
  const idx = v.constructor.types.indexOf(v.type)
  if(idx == -1) throw new TypeError('invalid value')

  return fs[idx](...valuesAsArray(v))
}

const cata = (fs, v) => fs[v.type](...valuesAsArray(v))
// we can also check if `fs` does not contain functions for all `v.constructor.types`
//
// `keys` from instance could be moved to to Type, e.g.:
// Tree.typeNames = ['Empty', 'Leaf', 'Node']
// Tree.typeKeys = [
//   [],
//   ['_1'],
//   ['_1', '_2', '_3'],
// ]
//
rjmk commented 8 years ago

Maybe we could have some general spec that would describe APIs of sum and product types? Something like a spec for daggy's cata method.

Some good comments by @robotlolita and @SimonRichardson on that in https://github.com/fantasyland/fantasy-land/issues/154

robotlolita commented 8 years ago

I'm not sure the spec describing specific data structures is a good idea, but as far as the description of tagged unions goes, something like OCaml's (and Lamdu's) Open Variants may be considered.

joneshf commented 8 years ago

Also using Either in chainRec is not a quite good idea imo. For example recently I saw there is an elm module elm-tail-recursion which uses Left as done and Right as next, when in old version of purescript-tailrec Left was used as next and Right as done. In current version of purescript-tailrec we have data Step a b = Loop a | Done b which I think better than Either.

Let me try to provide more motivation for my decision. I've found that if you type tailRec as (a -> Result a b) -> a -> b, (a -> Either a b) -> a -> b, or (a -> Step a b) -> a -> b, then the function is harder to use.

This is especially noticeable in PureScript because the Functor hierarchy works on the last type variable. We also lose most of the benefit of do notation.

If you break the recursion up into smaller functions and try to compose your functions, you end up having to complicate the problem a bit in order for things to line up. This is why go :: (Either Int Int -> Step Boolean (Either Int Int)) here. Compare that to my example here.

If you have (a -> Either b a) -> a -> b then you can rely on do notation pretty nicely:

foo = tailRec go
  where
  go x = do
    y <- bar x
    z <- baz y
    Left ("Barring " <> show x <> " with a bazzed " <> show y <> " gives " <> show z)

Whereas, with (a -> Either a b) -> a -> b you have to jump through some hoops. You can do things explicitly:

foo = tailRec go
  where
  go x =
    case bar x of
      Right b ->
        Right b
      Left y ->
        case baz y of
          Right b ->
            Right b
          Left z ->
            Right ("Barring " <> show x <> " with a bazzed " <> show y <> " gives " <> show z)

But, that's just using Either a b backwards from what we're used to with the Functor hierarchy. If you alpha-rename Right <-> Left, any knowledgeable PureScripter would point you to do-notation. Not to mention that the Functor hierarchy extends to typeclasses like Comonad f, Filterable f, and Traversable f. You could build up a set of combinators for working in the backwards world, but it feels wrong to force a new API on someone rather than building upon what they already know.

As far as Step a b vs Either a b. Step a b currently has a very limited API, so users have to do more wrapping/unwrapping just to get feature parity with Either a b. You have to write a function a -> Either a b and then wrap it in a function Either a b -> Step a b. Doesn't seem like a fair trade-off to impose on the user.

The point I wish to get across is that we don't get much benefit from renaming each value constructor. It might look prettier, but it's also demonstrably more difficult to use. We get a good deal more if you line up the type variables to play better with our Functor hierarchy—no matter what you name the value constructors.

joneshf commented 8 years ago

It pains me that we even have to question whether it's valuable to talk about Either a b. People have shown for decades that it's a useful data type. We use Compose f g a in Traversable t, why not use Either a b in chainRec.

Also, how does this function work:

chainRec :: ChainRec m => ((a -> c, b -> c, a) -> m c, a) -> m b

Where do you get the m b? For that matter, where do you get m c and b?. m must be covariant, since it's in the Functor hierarchy, and the only other b is in negative position. Am I missing something?

rjmk commented 8 years ago

I can't think of any cases where c is not t a b

rpominov commented 8 years ago

I can't think of any cases where c is not t a b

This actually follows from the algebraic types algebra:

image https://www.youtube.com/watch?v=iXZR1v3YN-8

So pair of functions b -> a and c -> a is isomorphic to function Either b c -> a.

Not sure if this helps, I just though it's cool to mention 😄

SimonRichardson commented 8 years ago

As always @joneshf you put it way better than me...

joneshf commented 8 years ago

I hope that didn't come off negative. I'm not upset with any of the choices or comments anyone has made.

SimonRichardson commented 8 years ago

I found it very informative 😀

puffnfresh commented 8 years ago

I think I vote for Church-encoding, because specifying data types seems no different to just providing an implementation. Main problem I see is that lots of data types can not be encoded without talking about existential types, including this case.

It seems like chainRec should look like:

chainRec :: ChainRec m => (a -> m (forall c. (a -> c) -> (b -> c) -> c)) -> a -> m b
safareli commented 8 years ago

It seems like chainRec should look like:

chainRec :: ChainRec m => (a -> m (forall c. (a -> c) -> (b -> c) -> c)) -> a -> m b

why?

gcanti commented 8 years ago

specifying data types seems no different to just providing an implementation

Maybe an interface?

// just a sketch
interface Either<L, R> {
  left<L, R>(left: L): Either<L, R>;
  right<L, R>(right: R): Either<L, R>;
  isLeft(): boolean;
  isRight(): boolean;
  fromLeft(): L;
  fromRight(): R;
  of...
  map...
  ap...
  chain...
}
SimonRichardson commented 8 years ago

I don't think an interface is a good idea either.

rpominov commented 8 years ago

We would need to have at least interface + some laws I think.

gcanti commented 8 years ago

If we want to represent unions

Union(A, B, C, ...) = A U B U C U ...

and cartesian products

Product(A, B, C, ...) = A x B x C x ...

in a way that can be manipulated by JavaScript, but hiding the concrete implementation, doesn't mean we have to define functions, and then group them in interfaces?

interface Union2<A, B> {
  // constructors
  a(): Union2<A, B>;
  b(): Union2<A, B>;

  isA(): boolean;
  fromA(): A; // fromA(a(x)) = x

  isB(): boolean;
  fromB(): B; // fromB(b(x)) = x
}

interface Union3<A, B, C> {
  a(): Union3<A, B, C>;
  b(): Union3<A, B, C>;
  c(): Union3<A, B, C>;
  isA(): boolean;
  fromA(): A;
  isB(): boolean;
  fromB(): B;
  isC(): boolean;
  fromC(): C;
}

...etc...

interface Product2<A, B> {
  // constructor
  make(a: A, b: B): Product2<A, B>;
  // projections
  prjA(): A; // projA(make(x, y)) = x
  prjB(): B; // projB(make(x, y)) = y
}

...etc...

https://github.com/purescript/purescript-either/blob/master/src/Data/Either.purs#L228-L243

puffnfresh commented 8 years ago

@gcanti those data-types can be Church-encoded (pedantically, Boehm-Berarducci encoded, if we're using types) meaning they can be represented as functions.

type Maybe a = forall b. b -> (a -> b) -> b
type Either a b = forall c. (a -> c) -> (b -> c) -> c
function nothing(b, f) {
  return b;
}

function just(a) {
  return function(b, f) {
    return f(a);
  };
}

function left(a) {
  return function(l, r) {
    return l(a);
  };
}

function right(b) {
  return function(l, r) {
    return r(b);
  };
}

// Example
function eitherToMaybe(e) {
  return e(
    function(ignored) { return nothing; },
    just
  );
}
joneshf commented 8 years ago

It seems like chainRec should look like:

chainRec :: ChainRec m => (a -> m (forall c. (a -> c) -> (b -> c) -> c)) -> a -> m b

That makes more sense.

gcanti commented 8 years ago

@puffnfresh Yes, and it's a really interesting topic, but my point is (and I understand if you don't agree):

I'd prefer to not handle Church-encoded data-types in my code, if possible. I'd love to manipulate plain old Maybes, Eithers, etc...

Though maybe I'm off the track and in practice is not a problem at all

rjmk commented 8 years ago

I am in favour of Church/BB encoding. My normal solution to the "unfriendliness" would be to additionally expose friendly helpers, but that seems harder in the case of a spec.

Also, I don't see why you can't have

chainRec :: ChainRec m => (forall c. (a -> c, b -> c, a) -> m c, a) -> m b

and then the forall floats to the left and disappears.

joneshf commented 8 years ago

The forall can't float to the left and disappear. First, higher rank polymorphism doesn't work like that. Second, you need the higher rank polymorphism in order to convert the c into a b.

If you could get rid of it, you'd be tasked with somehow finding a useful function c -> b. and that's impossible assuming your type system is sound.

You can try implementing it in PureScript or Haskell if you'd like to see where it fails. The easiest data type to implement it for would be Identity a.

PureScript

import Prelude
import Data.Identity

class Bind f <= ChainRec f where
  chainRec :: forall a b c. ((a -> c) -> (b -> c) -> a -> m c) -> a -> m b

instance chainRecIdentity :: ChainRec Identity where
  ...

Haskell

class Monad f => ChainRec f where
    chainRec :: ((a -> c) -> (b -> c) -> a -> m c) -> a -> m b

instance ChainRec Identity where
    ...

Or just try to write it in flow/typescript if that's your thing.

rjmk commented 8 years ago

Thanks, Hardy, that's really useful!

First, higher rank polymorphism doesn't work like that.

Can you point me to somewhere to learn about that?

rjmk commented 7 years ago

Looks like I had the quantification rules exactly backwards. I was thinking scopes on the left could be extended across the whole of the right, but scopes on the right could not be extended to the left. This appears to be almost opposite to the actual case (barring name collisions).

I guess I would phrase my understanding of why this happens as "you lose necessary polymorphism if you extend the scope to the right"

gabejohnson commented 6 years ago

Resurrecting this one.

In https://github.com/fantasyland/fantasy-land/issues/154#issue-175243113 @gcanti wrote:

Would it be possible to add a requirement for all ADTs that conform to the Fantasy Land spec that they expose a cata/fold/[adt] method (where [adt] is a lower case version of the name of the ADT)?

I like this idea. I've been toying around with a few interfaces. It seems providing signatures for the data constructors and a folding function is sufficient for lib interop for the cases below:

-- Identity
Identity :: a -> Identity a
identity :: (a -> b) -> Identity a -> b

-- Tuple
Tuple :: a -> b -> Tuple a b
tuple :: (a -> b -> c) -> Tuple a b -> c

-- Maybe
Nothing :: Maybe a
Just :: a -> Maybe a
maybe :: b -> (a -> b) -> Maybe a -> b

-- Either
Left :: a -> Either a b
Right :: b -> Either a b
either :: (a -> c) -> (b -> c) -> Either a b -> c

Conversion functions between libs:

const convertId = A => B => A.identity(B.Identity) ;

const convertTuple = A => B => A.tuple(B.Tuple);

const convertMaybe = A => B => d => A.maybe (B.Nothing) (B.Just);

const convertEither = A => B => A.either (B.Left) (B.Right);

This spec requires that all provided functions are fully curried. In the world of arrow functions, I don't think this is too much to ask.

davidchambers commented 6 years ago

Our specification of the Maybe type in #278 was too prescriptive. It required that every value of type Maybe a have isJust :: Boolean, and that all those values but Nothing also have value :: a.

We then experimented with Church encoding, but this was equally problematic. One could not define List#fantasy-land/compact :: List (Maybe a) ~> () -> List a, for example, without knowing the specifics of the Maybe implementation. @gabejohnson proposed isJust and fromJust functions in https://github.com/fantasyland/fantasy-land/pull/278#discussion_r154383877, but these required the folding function (maybe :: b -> (a -> b) -> Maybe a -> b) as an argument. The link from a value of type Maybe a to the appropriate folding function was missing.

Specifying that the folding function must live on the type representative would ensure that one can get from m :: Maybe a to maybe :: b -> (a -> b) -> Maybe a -> b via m.constructor.maybe.

Here's a possible implementation of Array#fantasy-land/compact:

//  Array$prototype$compact :: Array (Maybe a) ~> () -> Array a
function Array$prototype$compact() {
  const result = [];
  for (let idx = 0; idx < this.length; idx += 1) {
    const m = this[idx];
    const maybe = m.constructor.maybe;
//                 ^^^^^^^^^^^^^^^^^^
    if (maybe(false)(x => true)(m)) {
      result.push(maybe(undefined)(x => x)(m));
    }
  }
  return result;
}

All this assumes is that the type representative provides the maybe function. :)

paldepind commented 6 years ago

@davidchambers

Our specification of the Maybe type in #278 was too prescriptive. It required that every value of type Maybe a have isJust :: Boolean, and that all those values but Nothing also have value :: a.

Why is that too prescriptive?

davidchambers commented 6 years ago

Why is that too prescriptive?

It precludes certain implementations. const Just = x => n => j => j (x);, for example, could not be used because n => j => j (x) does not have an isJust property.

paldepind commented 6 years ago

@davidchambers

Isn't const Just = x => n => j => j (x) also precluded by your suggestion as it results in values that don't have a m.constructor.maybe? If I defined Just like that and plugged Just(12) into an array and called the Array$prototype$compact you defined above I'd get a run-time error.

paldepind commented 6 years ago

I don't think precluding const Just = x => n => j => j (x) matters anyway. That implementation of Just is already precluded by Fantasy Land from implementing functor, monoid, monad, filterable, etc.

xaviervia commented 6 years ago

A quick comment about the isJust property.

It feels weird. The way I would expect to find out if the value I got is a Just or a Nothing (or a Left or Right in an Either for that matter) is to case-split on it, not to check the value of a property. I feels clean how FL specs only talk about functions right now. Wouldn't it be viable to go in the direction of

x.cata({
  Just: value => console.log(value),
  Nothing: () => console.log('It was a Nothing')
})

?

davidchambers commented 6 years ago

Isn't const Just = x => n => j => j (x) also precluded by your suggestion as it results in values that don't have a m.constructor.maybe?

You're absolutely right, Simon!

I agree that this is quite clean, @xaviervia:

Maybe.prototype.cata :: Maybe a ~> { Nothing :: () -> b, Just :: a -> b } -> b

I consider this to be even cleaner:

Maybe.maybe :: b -> (a -> b) -> Maybe a -> b

The advantage is that there are no labels. Those who prefer to think of “Some” and “None” rather than “Just” and “Nothing” are free to do so.

Specifying as little as possible seems wise. For this reason perhaps we should specify that the folding function on the type representative be named fantasy-land/cata or fantasy-land/fold rather than fantasy-land/{maybe,either,...}. This way we could avoid mentioning the name of the type in addition to the names of its data constructors. Those who prefer to think of “Option” rather than “Maybe” would be free to do so (we would still refer to Maybe in type signatures, of course).

paldepind commented 6 years ago

@davidchambers

So maybe isJust :: Boolean is not too prescriptive?

I think specifying a pattern matching like function results in a very nice API. But I also see some downsides.

I'd like for the Fantasy Land spec not to have a performance penalty. Requiring Maybes to have an isJust :: Boolean property exposes the "tag" in the sum type directly and avoids all the above problems. If one wants a different API then that can easily be implemented on top.

davidchambers commented 6 years ago

So maybe isJust :: Boolean is not too prescriptive?

Perhaps not, although it does expose the tag name.

If the maybe function is curried temporary functions will be allocated which creates garbage.

The function needn't be curried. I believe Gabe was considering usability, but one could expose a separate function for public use:

Maybe["fantasy-land/fold"] :: (b, a -> b, Maybe a) -> b
Maybe.maybe :: b -> (a -> b) -> Maybe a -> b
safareli commented 6 years ago

To inspect a Maybe you have to give cata/fold/match two functions. If these functions require anything from the surrounding scope they'll be closures which creates garbage.

you could declare folding functions/values at the top level of your file, so they do not close over some values. and then use them to covert the maybe into some inspectable form and use it so no closure allocation is needed and only overhead is calling a function + constructing resulting object or whatever this folding functions return. if you are concerting them to some specific maybe type you can first check if it's instance of that type in which case you do not need to call cata/fold/.. on it

gabejohnson commented 6 years ago

@paldepind

Isn't const Just = x => n => j => j (x) also precluded by your suggestion as it results in values that don't have a m.constructor.maybe?

But Just = x => n => decorateJust(j => j(x)) where decorateJust adds a constructor and any other methods one would want would be fine. The point isn't that particular implementation, it's prescribing an implementation at all.

I don't think precluding const Just = x => n => j => j (x) matters anyway. That implementation of Just is already precluded by Fantasy Land from implementing functor, monoid, monad, filterable, etc.

There should be no specification that an ADT implement any of the FL algebras.

isJust :: Boolean is arbitrary and suggests we'd require these boolean properties on every value of a sum type. Consider the following

-- These
This :: a -> These a b
That :: b -> These a b
These :: a -> b -> These a b

Which flags should we choose? isThis and isThat? isThese and isThis?

These.cata :: (a -> c) -> (b -> c) -> (a -> b -> c) -> c

Takes This gets around the issue.

Also, avoiding a folding function would require specifying either fromJust :: Just a -> a or fromMaybe :: a -> Maybe a -> a.

This proposal isn't meant to be restrictive. Library authors are free to implement any other functions/methods/properties they want. And they don't have to be built on top of the folding function.

@xaviervia, @davidchambers fantasy-land/cata works for me as it could be added to Array for example. Also having a single name is nice.

@davidchambers

The advantage is that there are no labels. Those who prefer to think of “Some” and “None” rather than “Just” and “Nothing” are free to do so.

Just and Nothing would still be required, otherwise you have no way of constructing the data. Having standardized names would help avoid confusion for newcomers to functional programming (there's enough of that already).

i-am-tom commented 6 years ago

... Because I got pinged: I like the Church idea, but could be convinced of formalising cata. At the end of the day, this is perfectly sufficient as an implementation:

const Just = x => _ => f => f(x)
const Nothing = x => _ => x

Anything else (again, with the possible exception of a cata-esque function (though remember it isn't a catamorphism) is more detail than is necessary. Aside from anything else, I don't need to know if something is a Just if I can say isJust = m => m(true)(_ => false).

🏃

davidchambers commented 6 years ago

The advantage is that there are no labels. Those who prefer to think of “Some” and “None” rather than “Just” and “Nothing” are free to do so.

Just and Nothing would still be required, otherwise you have no way of constructing the data.

Just and Nothing would still be required to construct values, yes, but Array$prototype$compact and other functions which interact with existing values would not need to reference the data constructors.

[To determine whether] something is a Just […] I can say isJust = m => m(true)(_ => false).

Who is providing m, the folding function? If I am defining List#fantasy-land/compact, say, I have no idea how to define the appropriate folding function for the (unknown) Maybe implementation. Therefore, I need a way to get from a value of type Maybe a to this folding function, which suggests that Church encoding is insufficient (but could work with the help of a decorator, as Gabe suggested).

i-am-tom commented 6 years ago

The Maybe is the folding function :D type Maybe a = forall r. r -> (a -> r) -> r

You don't have to "get" anywhere if everything is done on primitive Church encoding. Leave the library to find pretty words for things, but the spec to encode the bare necessities.

davidchambers commented 6 years ago

The Maybe is the folding function :D type Maybe a = forall r. r -> (a -> r) -> r

Aha! I see it now. Very cool!

You don't have to "get" anywhere if everything is done on primitive Church encoding.

Requiring Church encoding seems problematic to me. As @paldepind observed, Church-encoded ADTs cannot provide fantasy-land/-prefixed methods, leading me to wonder whether we'd end up with one Church-encoded Maybe type and one Maybe type which implements various parts of the Fantasy Land spec, converting values from one type to the other as necessary.

gabejohnson commented 6 years ago

I feel like we're getting close. How about a function or method which transforms the value into it's Church-encoded representation?

maybe :: Maybe a ~> b -> (a -> b) -> b
MyLib.Just(42).maybe (OtherLib.None) (OtherLib.Some)
safareli commented 6 years ago

Church-encoded ADTs cannot provide fantasy-land/-prefixed methods,

Functions are objects and/mutate props on them. I'm not saying that we should use one church encoded maybe tho. If a maybe is implemented using church encoding it might overflow stack on some operations, like this:

instance Functor ChurchMaybe where
    fmap f (ChurchMaybe x) = ChurchMaybe $ \n j -> x n (j . f)
paldepind commented 6 years ago

@davidchambers

Requiring Church encoding seems problematic to me. As @paldepind observed, Church-encoded ADTs cannot provide fantasy-land/-prefixed methods, leading me to wonder whether we'd end up with one Church-encoded Maybe type and one Maybe type which implements various parts of the Fantasy Land spec, converting values from one type to the other as necessary.

I completely agree. Specifying that the Maybe itself should be church-encoded is the most prescriptive of the ideas discussed so far. It means that there is essentially only one way to implement a Maybe. And furthermore, that way is incompatible with the rest of the specification (unless one counts monkey-patching the created functions). It seems odd to specify abstractions that data-types can implement and then specify data-types that are incompatible with the very abstractions we want them to implement.

@gabejohnson

I feel like we're getting close. How about a function or method which transforms the value into it's Church-encoded representation?

I think that is a good idea. It is almost the same as what David suggested except the method lives directly on the Maybe. To me that seems more convenient.

There should be no specification that an ADT implement any of the FL algebras.

That is not what I meant. My point was just that the various specifications should be compatible with each other. But, now that you're stating it, I'm wondering: why not? If we did specify that Maybe should implement the relevant abstractions that whould make it a lot easier to work with an arbitrary FL Maybe.

paldepind commented 6 years ago

@gabejohnson

isJust :: Boolean is arbitrary and suggests we'd require these boolean properties on every value of a sum type. Consider the following

Yes, you're right that isJust is arbitrary. If there are more than two constructors in the sum type one couldn't use booleans as the tag but would have to use numbers instead. But still, just as any inductive data type can be Church encoded it can also be represented as an object with a tag. The two representations would be isomorphic but, used in practice, they both have pros and cons. One of the downsides to the Church encoding is the performance overhead caused by the additional function calls. If that can also lead to stack-overflows as @safareli mentions then it is a serious issue.

gabejohnson commented 6 years ago

I feel like we're getting close. How about a function or method which transforms the value into it's Church-encoded representation?

I think that is a good idea. It is almost the same as what David suggested except the method lives directly on the Maybe. To me that seems more convenient.

@paldepind having a 'fantasy-land' prefixed method would have the added benefit of allowing other JS values to encode a specified type.

Array.prototype['fantasy-land/maybe'] = function (x, f) {
  return this.length === 0 ? x : f(this[0]);
}

var safeHead = m => m['fantasy-land/maybe'](Nothing, Just);

safeHead([]) // Nothing
safeHead([42]) // Just(42)

A specification for Maybe could look like:

Maybe

The Maybe type encodes the concept of optionality (Nothing and Just a).

If m has a Plus, the following law must hold:

m.maybe(m.constructor.zero(), m.constructor.of) === m (Plus identity)

maybe method

maybe :: Maybe m => m a ~> (b, (a -> b)) -> b

A value which conforms to the Maybe specification must provide a maybe method. The maybe method takes two arguments:

m.maybe(x, f)

  1. x is the value returned if m corresponds to Nothing

    1. No parts of x should be checked.
  2. f must be a binary function. It is called if m corresponds to Just

    1. if f is not a function, the behaviour of maybe is unspecified.
    2. f must return a value of the same type as x.
    3. No parts of f's return value should be checked.
safareli commented 6 years ago

@gabejohnson 👍 Array example peaty nice