I’m considering writing a talk about positionality in Haskell - that is, how the meanings of things like function arguments, data constructor arguments, type parameters, type class parameters, etc are often determined by their position in the data/function/class etc declaration (as opposed to, say, a name, as they would have in a data type declared using record syntax, or as a function argument would have in a language that supports keyword arguments), and what the tradeoffs of this are. I have a good understanding of these tradeoffs already, so I’m not asking for those to be explained in this thread - rather, I’m trying to collect examples of existing posts, talks, or discussions on this topic. If you know of any, please let me know! I’m sure people have written/spoken about this before but I’m struggling to find the right search terms.
I’d look over on /r/programminglanguages, with these searches you can find quite a few posts about it:
- ProgrammingLanguages: search results - keyword arguments
- ProgrammingLanguages: search results - named arguments
- ProgrammingLanguages: search results - positional arguments
That second search turns up this blog post about Dhall:
Not really a discussion, but Lean 4 embraces named and default arguments: https://github.com/leanprover/lean4/blob/master/doc/lean3changes.md#function-applications
Rich Hickey has dunked on Haskell for being very positional in “Maybe Not” (https://m.youtube.com/watch?v=YR5WdGrpoug) and the criticism is justified.
You’re free (for now) to build a time machine to go back to 1987:
- People don’t care much for using names
- People don’t care much for “positionality”
Well guess what? You can’t get rid of both, otherwise confusion reigns supreme. Considering the “positionality” of the ordinary lambda calculus seen practically everywhere these days, is it any great surprise that a language based on it is also so “positional”?
And I think this is the reason why positionality really bites us at the type level: we don’t have the lambda calculus at our hands! I.e. we do not have type-level lambdas. If we want to make a parameter of a type constructor functorial, it has to be at the last position. Mathematically this is quite unnatural: what I often want to say is that some type constructor is functorial “in a and b” and contravariant “in c and d”, but I can’t. In this instance I would therefore prefer named arguments to type constructors instead of positional arguments.
[…] we do not have type-level lambdas.
…my mistake - after seeing records and fields mentioned in the transcript for that presentation by Hickey for the third time, I stopped reading and simply assumed his criticism of Haskell was connected in some way to its ongoing records saga.
As for sort type-level lambdas - from 2018:
…while it isn’t the paper I was looking for, it does pose the same question - what happened?
Case in point, though: Hickey doesn’t seem to be a fan of static type systems at all, and I’d argue that named arguments are much more important for survival when you don’t have types.
Could @DavidB explain his concerns with an example please?
Aren’t Type Synonyms the mechanism to switch the order of args to an underlying Type Constructor? The downside is you can’t partially apply a Synonym (usually).
It maybe gets tricky if your Constructor is a GADT.
Sure. What I mean is the following example:
data F a b c = MkF { fst :: a, snd :: b -> Int, thd :: c }
Both morally and mathematically it is correct to say that F is a functor in a and c, and contravariant in b. But due to the way that the order of type arguments to type constructors matter, and also due to how the Functor typeclass is defined, I can only make F a functor in the last argument, i.e. c. And whenever I design a data type I have to think hard about which argument should be the one I can implement Functor for, and then I have to make that the last parameter. Type synonyms let me define something like type G a b c = F c b a, but this does not help for the concrete problem of typeclass instances.
On the termlevel we can always change the position of arguments locally with a lambda, like g = \a b c -> f c b a, so positionality is not so important. But we cannot do that on the typelevel, since we cannot write something like instance Functor (\a b c -> F c b a)instance Functor (\c -> F c x y) in order to make F an instance of Functor in its first argument.
The following is purely speculative; I don’t have any concrete ideas for how this should work syntactically, but if the type arguments to a type constructor were passed in some sort of structural record, like data F :: { a :: Type, b :: Type, c :: Type } -> Type = ..., then it might be possible to declare F an instance of Functor in both a and c.
Edit: This is all just meant to show that the order of arguments is much more important on the type level than on the term level 
I am actually a big fan of ImplictParams, which gives you named function parameters that look like constraints.
Thanks for explaining further. (And apologies I’m not finding time to reply fully.) So we can’t make a instance Functor for a Type Synonym, because Functor is a Constructor Class and in the decl we must omit the last argument to the Constructor.
You’re not so omitting in that decl using type-lambda. So I think your example won’t work as given – even supposing we have type-lambdas.
You are right, the type constructor was underapplied, I fixed it. The fundamental reason why we will probably never have these instances with type lambdas is that the GHC developers are probably extremely reluctant to implement higher-order unification (for good reasons!). But an approach with named type arguments instead of positional type arguments can probably circumvent this problem, but again, this is very speculative on my side.
It wouldn’t be that hard to do this as a library.
{-# LANGUAGE AllowAmbiguousTypes, DataKinds, RecordWildCards, TypeFamilies #-}
import Data.Functor.Contravariant
--- Library code
class FunctorIn lbl fx where
type FISubst lbl fx a
fmapOver :: (a -> b) -> FISubst lbl fx a -> FISubst lbl fx b
class ContravariantIn lbl fx where
type CISubst lbl fx a
contramapOver :: (b -> a) -> CISubst lbl fx a -> CISubst lbl fx b
newtype AsFunctorIn lbl fx a = AsFunctorIn { unAFI :: FISubst lbl fx a }
newtype AsContravariantIn lbl fx a = AsContravariantIn { unACI :: CISubst lbl fx a }
asFunctorIn :: forall lbl fa a. (fa ~ FISubst lbl fa a) => fa -> AsFunctorIn lbl fa a
asFunctorIn = AsFunctorIn
asContravariantIn :: forall lbl fa a. (fa ~ CISubst lbl fa a) => fa -> AsContravariantIn lbl fa a
asContravariantIn = AsContravariantIn
instance FunctorIn lbl fx => Functor (AsFunctorIn lbl fx) where
fmap f (AsFunctorIn a) = AsFunctorIn (fmapOver @lbl @fx f a)
instance ContravariantIn lbl fx => Contravariant (AsContravariantIn lbl fx) where
contramap f (AsContravariantIn a) = AsContravariantIn (contramapOver @lbl @fx f a)
--- User code
data F a b c = MkF { fst :: a, snd :: b -> Int, thd :: c }
instance FunctorIn "a" (F a b c) where
type FISubst "a" (F a b c) a' = F a' b c
fmapOver f MkF{..} = MkF{ fst = f fst, .. }
instance ContravariantIn "b" (F a b c) where
type CISubst "b" (F a b c) b' = F a b' c
contramapOver f MkF{..} = MkF{ snd = snd . f, .. }
instance FunctorIn "c" (F a b c) where
type FISubst "c" (F a b c) c' = F a b c'
fmapOver f MkF{..} = MkF{ thd = f thd, .. }
example :: F Char Int Bool
example = MkF 'x' (+ 1) False
example1 :: F String Int Bool
example1 = unAFI $ (: "") <$> asFunctorIn @"a" example
example2 :: F Char String Bool
example2 = unACI $ length >$< asContravariantIn @"b" example
The user instances are mostly boilerplate and could probably be generated by some TH functions. The newtype wrappers are certainly clunkier than first-class language support for multifunctors would be, but at least it doesn’t require any new syntax or extending the type system.
Wellll … You said earlier you wanted two instances for F. So
- What would the other one look like?
- How could the instance-checker be sure those are type-apart? Or are they Overlapping and in no substitution ordering ?
- At a usage site for
fmap, how would instance resolution know which instance to pick?
So although @rhendric’s newtype approach is clunky/needs a lot of boilerplate, I can at least see it has a good chance of working.