Have you had a chance to peruse the Andreas Rossberg 1ml paper on embedding first class modules into f omega that has been circulating? Perhaps there are ideas There that could be adapted. Especially since core is an augmented f omega

On Saturday, April 25, 2015, Ertugrul Söylemez <ertesx@gmx.de> wrote:

>>> hrm, wouldn't your proposed extension be largely accomplished by
>>> using Record pun and Record WildCards?
>>
>> A part of it would, but it wouldn't preserve operators. For example
>> instead of `x r.<> y` you would have to write `(<>) r x y`.
>
> Not at all.
>
> three :: Integer
> three =
> let Monoid{..} = sum in
> 1 <> 2

Puns become tedious and error-prone as soon as you need to refer to
multiple records, when operators are involved. But it's not that
important actually. I can live with the current record syntax.

The most useful features would be defaults, a more suitable syntax for
defining record types and potentially the following:

>> Other class features are not accessible, most notably type-level
>> features like associated types.
>
> Associated types become additional type variables of the record type.

Indeed. However, when the type follows from other type arguments, it
would often be convenient not to spell it out and instead bring an
associated type constructor into scope. This is especially true when
the AT refers to a type that isn't used very often.

record Extractor a where
type Elem a
extract :: a -> Maybe (Elem a, a)

extractTwo
:: (e1 : Extractor a)
-> (e2 : Extractor a)
-> a
-> Maybe (e1.Elem a, e2.Elem a, a)
extractTwo e1 e2 xs0 = do
(x1, xs1) <- e1.extract xs0
(x2, xs2) <- e1.extract xs1
return (x1, x2, xs2)

> But the functional dependency is not enforceable on the value level
> (isn't the whole point of this discussion not to restrict what
> "instances" can be defined), so you end up with
>
> class C a t,
>
> a simple MPTC.

I don't see a reason to enforce a dependency, since there is no
equivalent to instance resolution. Regular unification should cover any
ambiguities, and if it doesn't you need ScopedTypeVariables.

>> The idea is that a record would be completely equivalent to a class
>> with the only difference being that you define values instead of
>> instances, that there are no constraints on which values can exist
>> and that those values must be passed explicitly to functions as
>> regular arguments.
>
> Except we already have regular records (aka data types) which satisfy
> 90% of the requirements, and adding another language construct to
> satisfy those remaining 10% feels wrong to me. I'd rather improve the
> existing construct.

That's actually what I'm proposing. The record syntax would simply be
syntactic sugar for single-constructor data types that is more suitable
for records, especially when defaults and other class-like features are
involved. Most notably it would support layout. There is no reason why
you shouldn't be able to use `data` to achieve the same thing, except
with a clumsier syntax and the option to have multiple constructors.

Greets,
Ertugrul