Isn't your associated type here more like a dependent record field/ existential that we can kinda expose?<div><br></div><div>This does seem to veer into first class module territory.  Especially wrt needing first class types in a fashion. </div><div><br></div><div>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<span></span><br><br>On Saturday, April 25, 2015, Ertugrul Söylemez <<a href="mailto:ertesx@gmx.de">ertesx@gmx.de</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">>>> hrm, wouldn't your proposed extension be largely accomplished by<br>
>>> using Record pun and Record WildCards?<br>
>><br>
>> A part of it would, but it wouldn't preserve operators.  For example<br>
>> instead of `x r.<> y` you would have to write `(<>) r x y`.<br>
><br>
> Not at all.<br>
><br>
>   three :: Integer<br>
>   three =<br>
>     let Monoid{..} = sum in<br>
>     1 <> 2<br>
<br>
Puns become tedious and error-prone as soon as you need to refer to<br>
multiple records, when operators are involved.  But it's not that<br>
important actually.  I can live with the current record syntax.<br>
<br>
The most useful features would be defaults, a more suitable syntax for<br>
defining record types and potentially the following:<br>
<br>
<br>
>> Other class features are not accessible, most notably type-level<br>
>> features like associated types.<br>
><br>
> Associated types become additional type variables of the record type.<br>
<br>
Indeed.  However, when the type follows from other type arguments, it<br>
would often be convenient not to spell it out and instead bring an<br>
associated type constructor into scope.  This is especially true when<br>
the AT refers to a type that isn't used very often.<br>
<br>
    record Extractor a where<br>
        type Elem a<br>
        extract :: a -> Maybe (Elem a, a)<br>
<br>
    extractTwo<br>
        :: (e1 : Extractor a)<br>
        -> (e2 : Extractor a)<br>
        -> a<br>
        -> Maybe (e1.Elem a, e2.Elem a, a)<br>
    extractTwo e1 e2 xs0 = do<br>
        (x1, xs1) <- e1.extract xs0<br>
        (x2, xs2) <- e1.extract xs1<br>
        return (x1, x2, xs2)<br>
<br>
<br>
> But the functional dependency is not enforceable on the value level<br>
> (isn't the whole point of this discussion not to restrict what<br>
> "instances" can be defined), so you end up with<br>
><br>
>   class C a t,<br>
><br>
> a simple MPTC.<br>
<br>
I don't see a reason to enforce a dependency, since there is no<br>
equivalent to instance resolution.  Regular unification should cover any<br>
ambiguities, and if it doesn't you need ScopedTypeVariables.<br>
<br>
<br>
>> The idea is that a record would be completely equivalent to a class<br>
>> with the only difference being that you define values instead of<br>
>> instances, that there are no constraints on which values can exist<br>
>> and that those values must be passed explicitly to functions as<br>
>> regular arguments.<br>
><br>
> Except we already have regular records (aka data types) which satisfy<br>
> 90% of the requirements, and adding another language construct to<br>
> satisfy those remaining 10% feels wrong to me. I'd rather improve the<br>
> existing construct.<br>
<br>
That's actually what I'm proposing.  The record syntax would simply be<br>
syntactic sugar for single-constructor data types that is more suitable<br>
for records, especially when defaults and other class-like features are<br>
involved.  Most notably it would support layout.  There is no reason why<br>
you shouldn't be able to use `data` to achieve the same thing, except<br>
with a clumsier syntax and the option to have multiple constructors.<br>
<br>
<br>
Greets,<br>
Ertugrul<br>
</blockquote></div>