As the title suggests I'm trying to implement an arbitrary degree blackbird combinator (something I'd always wanted but could never have in Haskell), that is:
bird : (n : Nat) -> (x -> y) -> (a1 -> a2 -> ... -> an -> x) -> a1 -> a2 -> ... -> an -> y
bird k f g x1 ... xk = f (g x1 ... xk)
bird 0 = (&)
bird 1 = (.)
bird 2 = (.:)
But I've been flailing around for an eternity trying to get this to work. This is my first time writing Idris, apologies for the ignorance that ensues:
import Data.Vect
args : Foldable t => Type -> t Type -> Type
args = foldr (\acc, t => acc -> t)
And then two different implementations of my combinator (not tested at the same time!):
bird : {ts : Vect n Type} -> (n : Nat) -> (a -> b) -> args a ts -> args b ts
bird Z f = f
bird (S k) f g x = bird k f (g x)
bird : {ts : Vect n Type} -> (n : Nat) -> (a -> b) -> args a ts -> args b ts
bird k = foldr (.) id $ replicate k (.)
Yeilding this error
Error: While processing right hand side of bird. Can't solve constraint
between: a and foldrImpl (\acc, t => acc -> t) a id ts.
and this one,
Error: While processing right hand side of bird. When unifying:
?a -> a
and:
a
Mismatch between: ?a -> a and a.
respectively. Frankly I think part of the problem might be Idris's odd treatment of composition, for example, (.) . (.) has a vastly different type then it does in Haskell, and frankly it seems to me that Haskell got it right,
(.) . (.) : (?b -> ?c) -> (?a -> ?a -> ?b) -> ?a -> ?a -> ?c (Idris)
instead of
(.) . (.) :: (c -> d) -> (a -> b -> c) -> a -> b -> d (Haskell)
Thanks for your help!
That combinator already exists within the Idris2 standard library as chain. It's a bit more annoying to use than your version, as it always requires passing the argument types of the second function, but I guess that's as good as we can get now. By the way, the 0-ary combinator would be $, not &.
import Data.Fun
double : Int -> Int
double x = 2 * x
add : Int -> Int -> Int
add x y = x + y
doubleAdd = chain {ts=[Int,Int]} double add