Closed johnchandlerburnham closed 4 years ago
I think multiple solutions exist, but it is great to have conventions and recommended techniques. I don't like multi-line applications and think they should be avoided. My favorite solution is o use let
s to shorten lines. In this case, we can give short names to polymorphic instantiations, so option 2 is definitely my favorite, although I'd have it like this:
// Polymorphic instantiations of `apply`
let <a> = apply(~A, ~B)
let <b> = apply(~B, ~C)
let <c> = apply(~(B -> C), ~((A -> B) -> A -> C))
let <d> = apply(~(A -> B), ~(A -> C))
let <e> = apply(~A, ~C)
// Polymorphic instantiations of `pure` and `compose`
let pur = pure(~((B -> C) -> (A -> B) -> A -> C))
let cmp = F/compose(~A,~B,~C)
// Asserts that both side are equal:
u <b> (v <a> w) == pur(cmp) <c> u <d> v <e> w
Exploiting operators to have a Haskell-like equation in the end. We can't define operators with let
yet, though, but we should. In the case lines are too big and there are not enough polymorphic variables, my second favorite approach is to build a big line in chunks with a chain of let
s. As in:
// Builds left side, `u <*> (v <*> w)`
let lft_begin = v
let lft_apply_w = apply(~A, ~B, lft_begin, w)
let lft_u_apply = apply(~B, ~C, u, lft_apply_w)
let lft_side = lft_u_apply
// Builds right side, `pure (.) <*> u <*> v <*> w`
let rgt_begin = pure(~((B -> C) -> (A -> B) -> A -> C), F/compose(~A,~B,~C))
let rgt_apply_u = apply(~(B -> C), ~((A -> B) -> A -> C), rgt_begin, u)
let rgt_apply_v = apply(~(A -> B), ~(A -> C), rgt_apply_u, v)
let rgt_apply_w = apply(~A, ~C, rgt_apply_v, w)
let rgt_side = rgt_u_apply
// Asserts that `u <*> (v <*> w) == pure (.) <*> u <*> v <*> w`
lft_side == rgt_side
Anyway, I think introducing new names with let
s should be preferred over multi-line function calls almost always. Thoughts?
I really like doing <a>
,<b>
,<c>
a lot! Will that conflict with the use of <>
for unbox
though?
I agree that let
should be preferred to multi-line function calls, but it seems like there are some places where multiline is better. In Data.List.fm for example:
!map.composition*n :
!{~A : Type
, ~B : Type
, ~C : Type
, f : !{:B} -> C
, g : !{:A} -> B
, xs : List(A)
} -> <map*n(~B, ~C, f)>(<map*n(~A, ~B, g)>(xs)) ==
<map*n(~A, ~C, #{x}<f>(<g>(x)))>(xs)
case/List xs
| cons =>
cong(
~ List(C),
~ List(C),
~ <map(n, ~B, ~C, f)>(<map(n, ~A, ~B, g)>(tail)),
~ <map(n, ~A, ~C, #{x}<f>(<g>(x)))>(tail),
~ {xs} cons(~C, <f>(<g>(head)), xs),
~ map.composition(~A, ~B, ~C, f, g, tail))
| nil =>
refl(~nil)
: <map(step(n), ~B, ~C, f)>(<map(step(n), ~A, ~B, g)>(self)) ==
<map(step(n), ~A, ~C, #{x}<f>(<g>(x)))>(self)
* refl(~nil)
I don't think let
would help much. It's just an inherently noisy proof (with current syntax at least). So I think we should at least have a standard way to layout muti-line function calls, even if the guidance is to prefer let.
(Incidentally, map.composition
is an example of <f>
being used as unbox(f)
.)
My preferred style for multi-line function calls is to say
foo(
a
, b
, c
)
with commas and close-paren aligned with the first letter of the function name. We could decide to say "one arg per line" or allow programmers to combine lines as they see fit, provided that the initial comma in the line aligns:
foo(a,b
, c
, d
)
foo(a
, b, c
, d
)
outdated
We need a consistent style convention for what to do when a function grows past a single line.
In Control.Applicative.fm, we have the composition law for applicative functors:
Which is eqivalent to the (pseudo) Haskell:
There are a number of possibilities here, but my two preferred ones are
lets
are optional to abstract long expressionsapply(~B, ~C, u, apply(~A, ~B, v, w)) == apply(~A, ~C , apply(~(A -> B), ~(A -> C) , apply(~(B -> C), ~((A -> B) -> A -> C), cmp , u ) , v ) , w )
But there are many many variations. The important thing is that we need a consistent style guide that is easy to define and apply and produces legible code.
One variant of option 2 is to say "If you abstract some polymorphic functions in an expression, you have to be consistent and abstract all of them." So the mixed
au
andapply
from suggestion 2 above would be changed to: