Sneak Peek: Bolt Math

One other thing to note: Since Function has a fundep, I think that the associated type family return could be written as

class Function r {- arity ? -} args | r -> {- arity ? -} args where
    type Return r :: Type

I think this is a bit simpler and makes less typing (keystrokes, not types) needed About variadic functions:

ApothecaLabs:

I didn’t want to rule out support for variadic functions! I haven’t written code to demonstrate handling them, but it should be fairly trivial - you repeat the last argument type indefinitely until the arity runs out, and viola, variadic functions

This is my effect on making a variadic function like what you describe.

type Repeat :: Nat -> k -> [k]
type family Repeat n a where
    Repeat 0 _ = []
    Repeat n a = a : Repeat (n-1) a
type family Call' (args :: [Type]) out :: Type where
    Call' '[] out = out
    Call' (a ': args) out = a -> Call' args out

type Call :: Nat -> [Type] -> Type -> Type
type family Call arity args out where
    Call 0 '[a] out = TypeError ('Text "Arity can't be less than list of arguments")
    Call n '[a] out = Call' (Replicate n a)
    Call 0 '[]   out = out
    Call _ '[]   out = TypeError ('Text "Arity can't be less than list of arguments")
    Call n (a ': args) out = a -> Call (n-1) args out

I think the current implementation would be something like this

-- Hypothetical example, not realistic
data SubtractOrAddn n
instance Function (SubtractOrAddn n) n '[Bool,Int] where
    type Return (SubtractOrAddn n) = Int -- Assumes Return only takes in the r
    call :: Call n '[Bool,Int] (Return SubtractOrAdd4)
    call True = manyfoldl' (n - 1) (+) 0 -- This requires a surprising amount of type hackery to do, as well as knowledge of CPS.
-- We also assume RequiredTypeArguments was used to define manyfoldl'
    call False a = manyfoldl' (n - 2) subtract a

-- One reason not to like is that we don't actually take in an '[Bool,Int].
-- Another is that one might think that
-- > call @(SubtractOrAddn 2) takes in 2 ints, but it only takes in 1.
-- This isn't apparent from the definition (imo)

This could be done instead:

instance (x ~ Bool ': Repeat (n-1) Int) => Function (SubtractOrAddn n) n x where
    type Return (SubtractOrAddn n) = Int
    call = -- Same thing,

This has the advantage of no special casing of Varidic functions in the class, and still allows users to make variadic functions, with no loss of generality! It’s also very clear in the implementation that the Int is repeated n-1 times. Also, variadic functions require a large amount of type level shenanigans to even implement, so I’d be very surprised if many users decide to implement them. If you want, I can share my code for creating them. e.g. stuff like mayfoldl’. It took me a while to make so I’d be more than willing to share it with anyone (assuming I’d be referenced in the package).