[Haskell-cafe] Class-like features for explicit arguments

[Carter Schonwald]

Isn't your associated type here more like a dependent record field/
existential that we can kinda expose?

This does seem to veer into first class module territory.  Especially wrt
needing first class types in a fashion.

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 at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150425/fcd7fc97/attachment.html>