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
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