Explore possibilities for modular implicits

[brendanzab]

At the moment module polymorphism is kind of clunky. Whilst our priority is more focused on polishing what we already have, it might be good to note down our thoughts here.

Some references:

• Modular Implicits (paper)
• Modular Typeclasses (paper)
• ocamllabs/ocaml-modular-implicits
• 1ML – Core and Modules United
• On the Bright Side of Type Classes: Instance Arguments in Agda
• First-Class Type Classes

[brendanzab]

Here is an idea that uses row polymorphism to implement module inheritance, and a limited form of dependent types for accessing the associated fields on the module. You can think of [..] as forall.

type (f: Functor) =
    { t : Type -> Type
    , map : [a, b] -> (a -> b) -> f.t a -> f.t b
    }

type (f: Applicative) =
    { Functor
    | apply : [a, b] -> f.t (a -> b) -> f.t a -> f.t b
    , wrap : [a] -> a -> f.t a
    }

type (m : Monad) =
    { Applicative
    | flat_map : [a, b] -> (a -> m.t b) -> m.t a -> m.t b
    }

let (>>=) : [m : Monad, a, b] -> m.t a -> (a -> m.t b) -> m.t b
    (>>=) [m] = flip m.flat_map

let implicitly_typed = (>>=) f xs
let explicitly_typed = (>>=) [m = list_monad] f xs

Not sure how well (>>=) f xs would be inferred though! :o

• A polymorphic type system for extensible records and variant (paper)
• Extensible records with scoped labels (paper)

[brendanzab]

One issue with the above is how to handle multi-parameter module inheritance.

Maybe:

type (t : Traversable) =
    { functor : Functor
    , foldable : Foldable

    , t : t.functor.t & t.foldable.t

    , traverse : [f : Applicative, a, b] -> (a -> f.t b) -> t.t a -> f.t (t.t b)
    , sequence_a : [f : Applicative, a, b] -> t.t (f.t a) -> f.t (t.t a)
    , map_m : [m : Monad, a, b] -> (a -> m.t b) -> t.t a -> m.t (t.t b)
    , sequence : [m : Monad, a] -> t.t (m.t a) -> m.t (t.t a)
    }

where t & t is an intersection type.

Seems a little verbose though...

[brendanzab]

One issue with that last approach is traversing up the hierarchy to get to the function you want:

m.applicative.functor.map f xs

blegh

[Marwes]

m.applicative.functor.map f xs

Yeah that does not look fun. Row polymorphism might be useful here which purescript uses.

type Functor f = {
    map : (a -> b) -> f a -> f b,
    | r
}

type Applicative f = {
    map : (a -> b) -> f a -> f b,
    (<*>) : f (a -> b) -> f a -> f b,
    pure : a -> f a,
    | r
}

This would mean any Àpplicative is also a Functor.

With the ability to 'splat' records it might be pretty easy to write.

let applicative_list = {
    (<*>) = ..,
    pure = ...,
    .. functor_list // splat the functor instance into this record
}

https://leanpub.com/purescript/read#leanpub-auto-record-patterns-and-row-polymorphism

[brendanzab]

Your need another type parameter in your examples. ie:

type Functor (f : Type -> Type) (r : Row) = {
    map : (a -> b) -> f a -> f b,
    | r
}

[brendanzab]

Or did you mean:

type Functor f = forall (r : Row) . {
    map : (a -> b) -> f a -> f b,
    | r
}

[Marwes]

Actually I believe it should be.

type Functor f = forall r. {
    map : (a -> b) -> f a -> f b,
    | r
}

[brendanzab]

Interesting stuff in the 1ML paper - in some respects it looks strikingly similar to what you have arrived at in Gluon:

type MONAD (m : type => type) = {
    return a : a -> m a;
    bind a b : m a -> (a - > m b) -> m b
};

map a b (m : type => type) (M : MONAD m) (f : a -> b) (mx : m a) =
    M.bind a b mx (fun (x : a) => M.return b (f x))

They haven't addressed implicits yet (see section 7) or inheritance as far as I can see.

[brendanzab]

One interesting syntactic thing in 1ML is that:

type EQ = { type t; eq : t -> t };

desugars to:

EQ = type { t : type; eq : t -> t };

Giving the following insight:

The record type EQ amounts to a module signature, since it contains an abstract type component t. It is referred to in the type of eq, which shows that record types are seemingly “dependent”: like for terms, earlier components are in scope for later components – the key insight of the F-ing approach is that this dependency is benign, however, and can be translated away, as we will see in Section 3.

(Figure 1 is very enlightening as a summary)

[Marwes]

Definitely need to re-read the 1ML paper. While it does have some similarities gluon is much simpler currently as types in records can only be a single type.

type Test a = {
    F: Int -> Int // `F` is a unqiue type whereas in 1ML or Rust it may depend on `a`
}

I never quite got why 1ML allowed types to be used as values (or I did get it and forgot). Types shouldn't appear in the actual code that is executed (so they aren't values during actual execution) and you don't actually want to be able to pass around and modify types arbitrarily in a Turing complete language anyway as that makes inference impossible

[brendanzab]

Separating kinds, types, and values is what leads to Haskell and the MLs having these separate sub-languages for functions, ML-style functors, type constructors, and type classes. I also have a hunch that these separations are part of what confuses people about these higher order concepts. One of the key insights is that they are really just different perspectives on the same thing.

I think this does come at the expense of the complexity of maintaining decidability though. 1ML restricts this somewhat in order to get good type inference, as described in Section 2, under 'Predicativity'. We probably don't have the luxury of a huge amount of time to spend on complex proofs, etc, so it does depend on how strongly you want to have decidability in the type system. I'm not too fussed with it tbh, but I am sympathetic to the idea of unifying language constructs.

[Marwes]

There are probably to many useful constructs that are impossible if we take a hard stance on preserving decidability so I am not to attached to having a decidable type system. As long as inference is predictable and is able to give good errors it is fine to require some type signatures to help out. I'd even go a bit further to say that all exported bindings should have a type signature (which could be checked with a lint defaulting to error when a signature is missing).

[brendanzab]

Yeah - I think having good errors is critical. That is one of my concerns with too much language simplification and leaning on inference - the increased expressiveness may make it harder to provide useful feedback to the user.

[brendanzab]

So it seems that the language already has the ability to express interface inheritance ! 😲 (see #56)

 type Applicative f = {
    functor : Functor f,
    apply : f (a -> b) -> f a -> f b,
    pure : a -> f a
}

Of course we don't have the ability to express associated types though - we can only pass them through as type parameters.

[brendanzab]

Discussion of modular typeclasses for Purescript: purescript/purescript#1886

[Marwes]

Implicits in Agda https://github.com/bitonic/tog/wiki/Implicit-Arguments

[brendanzab]

Note that Agda calls their implicits 'instance arguments' (as opposed to 'implicit arguments'). But the stuff about unifying named arguments could still be relevant. It is important to consider whether we use a different search algorithm for instances though.