Modularity

Prior discussion:

Please kindly move modularity discussion here and not pollute issue threads which are specialized on their thread title (speaking to myself also, not to any specific person), so that we can have modularity discussion organized in a thread of its own.

@shelby3

@shelby3
Associated types are fine and they constrain types on type level not on runtime level, right? (example: type family in typeclasses, pokemon example)

@keean
I will try to recapture your problem with a code example (though, I'm not really familiar with ocaml), you can correct me, if I'm wrong:

signature EQ = sig
type t
val eq : t * t -> bool
end

structure EqInt = struct
type t = int
val eq = Int.eq
end

fun f (X : EQ) = struct
type t = X.t
val eq = X.eq
end

Function f should have a signature of the form EQ where type t -> EQ where type t
which can be erased even if the type t from X is not known explicitly.
Why?
Every time you construct a signature instance EQ with certain type t, the compiler will/could create a monomorphized function for it. When a module of type EQ is applied to f, the compiler should decide to pick the right function at compile time, which should be possible because of type inference.
Even if you change X.t from int to float (don't know if possible), you state the type for the type change of X.t explicitly in your code, which should be recognized by the compiler.
The only problem that arises is if you eval a type out of a string which is created from "outside":

string<-readline...
X.t=eval_to_type(string)

Because of this, most statically typed languages disallow such things.

@sighoya

@sighoya it would help if you referenced the problem you are questioning, I am not sure what you are trying to show or disprove?

I want to prove that dependent types are not needed for modules.

Edit:
reference

You example has no runtime polymorphism. You need to introduce an existential type, so that you want to run Eq over a list of existential values.

You mean something like this:

signature EQ = forall x sig
type t=[x]
val eq : t * t -> bool
end

or

signature EQ = sig
type t=[forall x]
val eq : t * t -> bool
end

I don't know if the latter is a valid syntax, but I mean a heterogenous list, i.e. contain values of different types.
In the case of the latter example, fun f with:

fun f (X : EQ) = struct
type t = X.t
val eq = X.eq
end

should have signature of EQ where t=[forall x] ->EQ where t=[forall x],

meaning that t is a list where the elements are of type: Variant Type(runtime Union Type) for which no type erasure and no dependent type is needed.

@sighoya

@sighoya

meaning that t is a list where the elements are of type: Variant Type(runtime Union Type) for which no type erasure and no dependent type is needed.

That is different because with a union type you are limited in which types you can put in. Given a "String|Int" you can only put a string or integer into the heterogeneous collection.

With an existential type we can specify the interface, say forall a . Eq a => a which allows any type that implements Eq to be put in the collection.

I can actually demonstrate the unsoundness without using an existential type, just think about polymorphic recursion. You cannot monomorphise a recursive polymorphic function.

@sighoya

@sighoya

should have signature of EQ where t=[forall x] ->EQ where t=[forall x],

This type is impossible because the type escapes the existential.

@keean

@keean wrote

That is different because with a union type you are limited in which types you can put in. Given a "String|Int" you can only put a string or integer into the heterogeneous collection.

Thats right, therefore Variant Type != Union Type
@keean wrote

With an existential type we can specify the interface, say forall a . Eq a => a which allows any type that implements Eq to be put in the collection.

Aha, here an existential takes the role of a trait/typeclass object.
@keean wrote

I can actually demonstrate the unsoundness without using an existential type, just think about polymorphic recursion. You cannot monomorphise a recursive polymorphic function.

Corner cases/Undecidable issues
Do you think the following is sound?:
(+) :: Int->Int->Int
Int.MAX+Int.MAX=Error?

@keean wrote

@sighoya

should have signature of EQ where t=[forall x] ->EQ where t=[forall x],

This type is impossible because the type escapes the existential.

Yes it breaks the rules of existentials.
Maybe: f::EQ where t=Variant -> EQ where t=Variant is a better fit
or left out the associated type with: f::EQ->EQ
Why is it so important to include the associated type in the type signature?

Further, I don't see the need for dependent types for module purposes but maybe you mean runtime polymorphism is inevitable, then yes.
Runtime polymorphism is indeed very useful.

@keean

@keean

If a module has an associated type, and a module is first class (can be passed to a function as a value) then the associated type must depend on the value passed to the function. This is clearly the definition of a dependent type.

But if the instance of the module’s type is statically known at the time when the value is applied at the call-site then it’s no different than applying typeclasses at the call-site. So are typeclass bounds dependent typing?

I guess it’s because we erase the instance’s type from the static knowledge when we assign it to a module signature (but have to reify it with runtime dispatch), thus we don’t track it statically? Isn’t that the analogous to assigning an object to an existential type thus erasing it from static tracking?

The key difference is when the type of the value can’t be known statically, then we need to track the type of a value at runtime with some form of runtime dispatch. Which is analogous to existential types with typeclasses.

What am I missing? Trying to understand why you see a problem with this form of dependent typing that you don’t see with typeclasses?

I can actually demonstrate the unsoundness without using an existential type, just think about polymorphic recursion. You cannot monomorphise a recursive polymorphic function.

Ditto cannot monomorphise typeclass bounds with polymorphic recursion. Have to use runtime dispatch. We had a discussion about that in the past on these issue threads.

@sighoya wrote:

Further, I don't see the need for dependent types for module purposes but maybe you mean runtime polymorphism is inevitable, then yes.

Well I think he may be defining dependent type correctly, yet I agree that seems like it’s just runtime polymorphism. And I am also wondering why he dislikes it given it seems to occur because of the inevitable need for runtime polymorphism.

I thought dependent typing was when we can check the values of a value statically?? With runtime polymorphism we’re not enforcing the type of the value statically. There’s no monomorphisation going on.

Ditto typeclass bounds with polymorphic recursion.

No typeclasses only depend on the type of the thing, not the value of the thing.

Now you would have the same problem if you had type-classes with associated types, but in Haskell they get around it by saying the associated types must be globally coherent with the type parameters of the type class instances. This makes the type-class type-parameters, and the associated types of that type-class form a type-family.

@sighoya

@sighoya a variant type is also limited in the types you can put into it (at least it is in OCaml). Without existentials (runtime polymorphism) polymorphic recursion can still cause problems with modules that requires dependent types to support.

Now you can have modules without dependent types, if you limit the language to having everything monomorphisable. This means no runtime polymorphism, no polymorphic recursion etc.

@keean

@keean wrote

@sighoya a variant type is also limited in the types you can put into it (at least it is in OCaml).

My thoughts were onto dlang's Variant Type.
You can also further restrict dlangs Variant Type to allow assignments of values of specific types (they call them Algebraic Type, in the same url I presented).
A variant type is a any type without the sh?t of inheritance.

Edit:
A typeclass/trait object can also be seen as a Variant Type which is bounded to the types implementing the trait/typeclass. In some situations, a trait object can also be a Union Type (compile time Variant Type), in which case monomorphization can applies.

@shelby3

I thought dependent typing was when we can check the values of a value statically?? With runtime polymorphism we’re not enforcing the type of the value statically. There’s no monomorphisation going on.

I thought depending typing was when we cannot check the type of a variable at compile time (statically), because the variable's type depends on the variable's value and maybe of other variables's values.
However we can pattern match over it and can follow different branches in which the compiler knows the type for each branch (when done rightly), though it can become tedious.

Dependent types are indeed very useful. Imagine a type called DeterminantNotZeroMatrix, which is defined at follows:

DeterminantNotZeroMatrix<Type eltype,Int n,Int m>={Matrix<eltype,m,n> mat |  det(mat)!=0}

Edit: ambigious use of m, changed it to mat.

Once constructed this kind of dependent type, we can invert this Matrix without to check every time if the matrix is invertible.

But @keean, I think you need a runtime polymorphic time rather than dependent typing

There is a proposal to add type classes to C#. The funny thing is that the proposed implementation of typeclasses looks like a lot of a light form of Modular Type Classes

@sighoya

@sighoya

My thoughts were onto dlang's Variant Type.
You can also further restrict dlangs Variant Type to allow assignments of values of specific types (they call them Algebraic Type, in the same url I presented). A variant type is a any type without the sh?t of inheritance.

This kind of variant is not modular, as there is no way to represent a universal type tag. This kind of variant requires Run Time Type Information, which is a big problem for me, as you lose type erasure (and theorems for free) as well. I can give more details why this is bad (or perhaps why I don't like it if I am being generous).

But @keean, I think you need a runtime polymorphic time rather than dependent typing

Runtime type information is worse (see above) with dependent typing we can still resolve issues at compile time. For example if we try and print a value of an associated type, we can add the "Print" constraint to that module. This can be propagated up to the interface specification for the current module such that we say the argument for this function must be an iterator where the ValueType of the iterator is printable. These are dependent types (because the type passed to print depends on the value of the module passed to the function) but we solve by placing constraints on the types which we propagate at compile time. The latest we would need to check these constraints is when linking a dynamically loaded module, we still retain type erasure and don't have to find a way to store types in memory at runtime.

I think its bad to store types in memory at runtime due to the Russel paradox. If every memory location has a type, and a memory location contains a type then the type of a type is a type and we have created the conditions for a paradox. Everything in memory at runtime is a value, now we can create a mapping from values to types, but we cannot do this globally, because with separate compilation we don't know what values other compilers assign to which types. So we have to locally map values to types which is what an OCaml variant does (a disjoint sum type).

@keean

@keean wrote

Runtime type information is worse (see above) with dependent typing we can still resolve issues at compile time. For example if we try and print a value of an associated type, we can add the "Print" constraint to that module.

Looks like for me you need a trait/typeclas object

@keean wrote

I think its bad to store types in memory at runtime due to the Russel paradox. If every memory location has a type, and a memory location contains a type then the type of a type is a type and we have created the conditions for a paradox.

The type Type is a meta type which is a non well founded set including itself

@sighoya

@sighoya Type-classes provide specialisation (as distinct from generalisation which is provided by parametric types). Modules generally provide separate compilation, data-hiding and specialisation. For this language it would seem bet to limit modules to separate-compilation and data-hiding. I guess the issue here is that Haskell has these kind of modules, and there are calls for it to implement something more full featured like ML modules. The question is whether these calls are justified, or whether they are from people that don't understand how to implement what they want with typeclasses?

@shelby3

The question is whether these calls are justified, or whether they are from people that don't understand how to implement what they want with typeclasses?

This is a good question, but it was not my intention to challenge if a module system is worthless for you. The point is that @shelby3 wrote that module parametrization should be constrained by signatures.
Why couldn't this be accomplished by typeclasses?

One thing i don't understand with typeclass is in the context of highly interactive applications where the function to be executed on an object depend on global state that are exterior to the object.

For example in photoshop the effect of a click depend on which tool and option is selected.

With OO paradigm, it's easy to have a global class and instanciate the good class/module when a global state change, and runtime polymorphism can achieve this.

With typeclass how it's made in haskell i have more hard time to see how to achieve this same thing.

I can see how typeclass can be useful for program that are designed like linear algebra, always having the same function applied on an input, and rather designed as monolithic thing.

Or typeclass would need to be sort of 'first class', and having a way to select the good set of function to use depending on runtime state. Which i don't see how it would be possible if typeclass function are monomorphized at compile time. With the dictionary thing it would seem more possible to load and use specific typeclass function depending on runtime state.

@sighoya

@sighoya wrote:

The point is that @shelby3 wrote that module parametrization should be constrained by signatures.
Why couldn't this be accomplished by typeclasses?

@keean he means typeclass bounds instead of signature bounds on modules. We would still retain typeclass bounds on functions also.

That’s a reasonable question, because my conjecture is that parametrised modules provide less fine-grained grouping of parametric generalization which provides some benefits such as less noisy repetition of typeclass bounds on function declarations. With monomorphisation then typeclass bounds on modules is equivalent to signature instantiation of modules.

I think you are correct. Application of typeclass bounds to instances doesn’t require function application.

Unless @keean objects, I will incorporate this into the proposed Zer0 grammar I’m close to completing.

Note @keean had mentioned using typeclasses as modules before.

Why didn’t Backpack think of this?

Ah probably because of Haskell’s canonicity which I have proposed to forsake. Canonicity is why I think they were forced to separate the module system into a different concept of signatures. Remember again that I recently identified “strong modularity” combined with existential quantification as the source of anti-modularity unsoundness, so my proposal to forsake canonicity has to avoid that combination. Haskell doesn’t have the non-disjoint, structural unions which I have proposed and unions may suffice and be superior for most of the use cases we would otherwise use existential quantification (and the unions are bound to typeclass bounds at application to a function call site, not in the union object itself as is the case for existential quantification so it side-steps the unsoundness with strong modularity).

@NodixBlockchain

@NodixBlockchain typeclasses don’t force immutability. If you want to change the pointer to the function to callback, AFAICT there’s nothing in typeclasses preventing that.

Once again you are raising an issue in the wrong thread. This is the Modularity thread. You should have asked that question in for example the Why Typeclasses issues thread.

Please try not to thread jack and take threads off topic. I want to be able to find relevant discussion. I would be more than happy to discuss this topic with you if you raise it in a thread that is more related to the topic you want to discuss.

I have reverted my typeclass modularity proposal back to the “subtypeclasses” concept but with module name prefix on instance selection.

That linked post explains our modularity ideas for typeclasses have an issue with existential quantification— i.e. runtime polymorphism other than bounded union dynamic polymorphism.

The reasons why associated (aka abstract) types of typeclasses can’t be replaced by HKT and multi-parameter typeclasses:

Associated types are output types of instances, thus putting instances in control instead of the environment of the function/procedure application/call site. HKT and multi-parameter typeclasses are inputs set by the environment. Thus associated types are generally necessary to invert the control over the types. Someone wrote:

Note: I am aware that one can express currently express type synonyms in much the same way that one does in Java (or C#, or Eiffel; see Garcia et al paper): by making them a type-parameter of the trait itself. Rust's type-inference system does make that workaround more palatable, but it seems natural to enable the developer to express what they mean more directly: These types are obligations of the implementation, much like the functions declared in the trait, and thus it makes sense to express them the same way.
A motivating example (c.f. also) of multidimensional slices.
The data type which may be hard-coded to a specific type which is parametric in the typeclass— e.g. the element type of a typeclass which the data type with the hard-coded element type can implement as for example a fold or sort interface.

For example to implement the map interface on a String requires knowing that the callback function takes a type Char but String has no type parameter Char. Compare how clumsy this is to implement in an OOP paradigm without typeclasses (and thus without associated types).
The original research paper for associated data types noted in §2.1 Self-optimising finite maps on pg. 2 that they provide a way for the instance to dictate an optimized data structure:
Such maps change their representation in dependence on the structure of the key type k used to index the map. We express this idea by defining a type class MapKey, parameterised by the key type, with an associated type Map as one of its components:
```
class MapKey k where
   data Map k v
   empty :: Map k v
   lookup :: k → Map k v → v

instance MapKey Int where
   data Map Int v = MapInt (Patricia:Dict v)
   empty = MapInt Patricia:emptyDict
   lookup k (MapInt d) = Patricia:lookupDict k d
```
And a research paper noted on pg. 54:

Explicitly specifying type arguments that represent associated types also leads to the introduction of unnecessary implementation dependencies. As explained above, four of the type arguments in the call to the breadth-first search algorithm in Figure 12 are associated types of the first type argument, the graph type. These types may represent internal implementation details of the graph type. At each call to the algorithm, however, these types must be explicitly specified. Consequently, changes that should be just implementation details in a data structure require changes to user code at the call sites of generic algorithms that pass that data structure as an argument.
Associated types are necessary when hidden (helper) parameters are needed.

Important post about default typeclass instances, overlapping problems, and alternative solutions that apply to modules.

The data type which may be hard-coded to a specific type which is parametric in the typeclass— e.g. the element type of a typeclass which the data type with the hard-coded element type can implement as for example a fold or sort interface.

For example to implement the map interface on a String requires knowing that the callback function takes a type Char but String has no type parameter Char. Compare how clumsy this is to implement in an OOP paradigm without typeclasses (and thus without associated types).

On further thought, that clumsiness is due to the incorrect design of map in that it returns the same type as the input collection.

Scala’s (arguably Martin Odersky’s) corner-case laden “solution” was affectionately referred to as The Longest Suicide Note Ever Written.

A better solution seems to be having map always output a sequence or an iterator for a sequence. And offer a fromSequence type-class for types that can be mapped. For performance reasons, I don’t agree with making map input a sequence. Instead make it a typeclass and provide an implementation for each input collection type.

So then we really don’t necessarily require associated types for handling this case. We could define strings to be class StringT<T extends Char> and type String = StringT<Char>. That is more fugly though than employing an associated type. Probably want to define Char to be wide enough to encode all Unicode glyphs.

@keean

On further thought (and realize Microsoft broke my ability to edit my prior comment post, or @keean removed my privileged to do so?), we don’t have to incur the inefficiency of forcing map to output a sequence type when we really intend to invoke fromSequence anyway. Simple declare the map type-class as a two parameter type-class that also inputs the type of its output. For unsupported output type combinations, the type-class instance will not be provided and thus the compiler will generate an error.

@shelby3

@shelby3 no changes in permissions from me, but maybe the defaults have changed?

I will try accessing from the laptop with newer versions of all browsers including IE, and report if I have the same problem.

@shelby3

@shelby3 IE is not a good browser, even Microsoft realised this and tried to fix in Edge. Edge is better if you have windows 10. I used to really like Chrome, but these days I tend to use Firefox. Why not install Firefox?

I meant Edge (not IE) on my 2017 model ASUS laptop running Windows 10. :shudder:

I hate Microsoft so much I do not even bother to remember the names of any of their new sh8t.

@keean

Late Binding of Interface vs. Modularity?

I wrote:

I have reverted my typeclass modularity proposal back to the “subtypeclasses” concept but with module name prefix on instance selection.

That linked post explains our modularity ideas for typeclasses have an issue with existential quantification— i.e. runtime polymorphism other than bounded union dynamic polymorphism.

I wrote:

Important post about default typeclass instances, overlapping problems, and alternative solutions that apply to modules.

I’ll re-summarize the issues in one place to make this easier to digest and come back to.

Type classes: confluence, coherence and global uniqueness

Global uniqueness of type class instances is required to insure a globally consistent semantics aka an abstract algebra. Non-eager (i.e. not wild goose chase exhaustiveness checking) intra-module confluence (aka consistent type checking) and intra-module coherence (consistent intra-module semantics) don’t guarantee global (i.e. total order, nor just inter-module partial orders) semantic coherence.
Open type families are not modular

Open type families or associated types allow instances to create types, i.e. output types. Thus incoherent inter-module instances with open type families or associated type can segfault. Some heuristics are proposed to prevent inter-module incoherence (and enforce the requisite uniqueness of instances required for the necessary inter-module partial orders coherence) without a global total order eager guarantee of global uniqueness.

The point is also made that global uniqueness and coherence sacrifices modularity. The suggestion is made that perhaps the culture of Haskell needs to change and forsake a globally consistent abstract algebra and by implication instead view type classes only as some spaghetti code and not for enforcing some invariants of an API.
http://blog.ezyang.com/2014/09/open-type-families-are-not-modular/#comment-20942

Discussion of how the ML programming language differs (c.f. also the Type Inference Issues section below), which afaics is essentially delaying static binding of interface until construction of an object instance as contrasted with OOP which statically binds interface to the data type where (in the case of nominal typing) the data type is declared and its supertype is not replaceable after declaration (or in the case of structural typing where the interface type is declared, c.f. also). I had also shared my thoughts about what I believe to be the undesirable tradeoffs of the 1ML research.

So while the ML approach has the advantage of being able to operate on data in more than one way (e.g. different Ord sorting partial orders) by multiplexing partial orders defined by the interfaces attached to objects at construction time analogous to the partial orders of OOP but later, static, interface binding — and note each consistent set of interfaces are abstract algebras defining a said partial order if they extend a common ML signature — ML has the disadvantage that an object can only be operated on in one way after the binding of interface upon construction of said object instance. Whereas (without some dubious extensions) Haskell can only ever operate on objects in one consistent way with a presumed (but not intractably compiler enforced) globally consistent coherence aka global abstract algebra, Haskell has the arguably pyrrhic “advantage” of delaying static, binding of an object instance’s interface until the function call site. We can construct objects and then elsewhere in our program add them to collections or unions and bind the interface invariant to the (collection’s or union’s) generic type parameter at function call sites. Whereas afaics ML could only plausibly (hypothetically) allow adding more interfaces to an already constructed object by changing its type which require an exclusive reference (a feature ML doesn’t have) in order to consume the prior type?

Similar to OOP, Haskell also offers early, static binding of interface known as existential quantification aka Rust’s trait objects. And like OOP these existential type class bound interface invariants are set statically when the existentially quantified data type is declared. But unlike OOP and more like ML, the implementations of these interfaces are delayed until the instance of the existentially quantified object is constructed — so when combined with generic type parameters the analogous delay as ML is achieved except that the specificity of the type is erased by the generic invariant. ML is much more explicit about types which some people find to be a disadvantage and others perhaps argue the benefits which result are an advantage.
I have attempted to devise proposals for merging late, static binding within partial orders of type class abstract algebras, to match ML’s capability while not binding to object instances at their construction as ML does. But any such proposal will not be fully interoperable with unbounded existentially quantified types, c.f. also. Unbounded existentially quantified types are also incompatible with multiparameter type classes (except where only 1 of the parameters is unbounded generic), so maybe I prefer to forsake them.

Given that type class invariants declared on function definitions are bound at function call sites (as contrasted with ML which binds interface to object types upon object construction), then partial orderings for type classes should be based on partial orders of bindings at function call sites.

To enforce partial orders of abstract algebras then we need inheritance of signature analogous to ML in the type class context, so I had proposed “subtypeclasses”. IOW, to form a consistent abstract algebra for ReverseOrd (synonymous with Backwards(OrdInt) in the aforelinked ML example) then we need to name it as a partial order of Ord so that each data type can only be implemented once and thus coherently for each “subtypeclass” such as ReverseOrd — i.e. no overlapping instances for and enforce global uniqueness of instances of each partial order “subtypeclass”.

Function definitions would require an Ord type class interface invariant, and function call sites could inject the additional invariant of ReverseOrd, so that modularity of specialization is achieved along with the latest binding of interface to objects at function call sites. This is not equivalent to placing the additional “subtypeclass” invariant on the type class interface requirements of the function definition that contains the said function call site(s), because the body of (i.e. implementatin of a) function might call a plurality of said function call sites, each with different specializations, e.g. ReverseOrd, ForwardOrd, AdditiveMonoid, MultiplicativeMonoid, etc..

The challenge is the balance between being overly explicit versus losing modularity due to being implicit with “subtypeclasses”.
1. Type classes with global canonicity (i.e. that have no “subtypeclasses”) don’t require lifting to explicit module parameters for noiseless, highly granular modularity and refactoring.
2. Whereas, “subtypeclasses” should be explicit module parameters for maximum composability. Or some implicit or default combined with explicit override model which trades-off some modularity specificity for less explicit explosion in number of module parameters. For example import a module or function from a module, and declare that all Ord at function call sites in that module or specific function are to be ReverseOrd where not otherwise specialized on call sites. Obviously either way, minimizing “subtypeclasses” use will minimize explosion in explicit specificity.

Note AFAICT Scala 3 is ostensibly not enabling said partial orders correctly.

Type Inference Issues

Yet another blog also written by the co-developer of the Haskell modularity project Backpack What’s a module system good for anyway? discusses the issues with abstracting over for example the numerous string types in Haskell (e.g. String, Text and ByteString) and claims that ML signatures with functors is superior to type classes:

Using type classes (3) to regain modularity may seem like an attractive approach. But this approach has both practical and theoretical problems. First and foremost, how do you choose which methods go into the type class? Ideally, you'd pick a minimal set, from which all other operations could be derived. However, many operations are most efficient when directly implemented, which leads to a bloated type class, and a rough time for other people who have their own string types and need to write their own instances. Second, type classes make your type signatures more ugly String -> String to StringLike s => s -> s and can make type inference more difficult (for example, by introducing ambiguity). Finally, the type class StringLike has a very different character from the type class Monad, which has a minimal set of operations and laws governing their operation. It is difficult (or impossible) to characterize what the laws of an interface like this should be. All-in-all, it's much less pleasant to program against type classes than concrete implementations.

Wouldn't it be nice if I could import String, giving me the type String and operations on it, but then later decide which concrete implementation I want to instantiate it with? This is something a [ML-like] module system [e.g. Backpack] can do for you!

[…]

If designing an effective and principled type class to capture what String, ByteString, and Text “have in common” is difficult, then why would designing a module signature to do the same thing be any easier? I think these are the same problem […]

Great question. I think if you wanted to design “one” module signature to capture string representations, you would certainly still have the same problem. However, in an Backpack or ML-like module system, it is a lot less expensive to have multiple module signatures than it is to have multiple type classes: to implement a new type class, you have to explicitly write an instance; but to implement a module signature, all you need is for the module to be set up in the right way.

In my mind they aren’t really the same problem, for a rather peculiar reason. Even though many of the functions in e.g. Data.Text can be easily written in terms of smaller components, nobody really thinks that users should have to do so themselves. Rather, users should be able to import Data.Text and have the full API available to them. However, nobody wants to use large monolithic typeclasses (like ListLike), and really nobody is interested in writing new instances of monolithic typeclasses. So while people are willing to write all the functions for the module, they aren’t willing to list them all again in a class interface. So hopefully there will be less resistance to using a module system like Backpack […]

[…]

In the end, I see ListLike and TextualMonoid as both essentially implementation details of the same idea, presenting slightly different interfaces. Both are typeclass-based, though, with all the baggage that brings. If Haskell had ML-style modules, most likely neither would have come into being.

https://www.reddit.com/r/haskell/comments/28v6c9/backpack_an_mllike_module_system_for_haskell/cierxc1

Among other things, it's very useful for library code where you don't want to decide on a concrete implementation for the user. For example, the functional graph library does this by having a Graph typeclass. This is important to support different usecases of the library.

Unfortunately, the typeclass-based solution to this problem is very awkward in practice, and messes up type inference consistently. Using it felt like I was fighting the system more than taking advantage of it. For things like this, a real module system would be a significant improvement.

What issues did you have with it? What made you feel like you were fighting it?

Mostly dealing with type inference, especially if I wanted my code to be generic over the graph implementation too. Ultimately, I just ended up using a concrete type in my code, which was unfortunate. I think there were some other minor annoyances, but it was a while ago so I don't remember exactly.

I discussed this with @keean and he seemed to concur with my point that Haskell’s type classes don’t have to be monolithic. Employ class inheritance to extend only those finely grained type classes required by each separate use case and automatically inherit the extant instance implementations, e.g.:

class Concat a b c where
  concat :: a -> b -> c

class  (Concat a a a, Ord a) => ConcatOrd a
instance  (Concat a a a, Ord a) => ConcatOrd a

Thus it appears that the claimed advantage for ML-like signatures and functors distills to some perceived advantage w.r.t. type inference.

Type inference ambiguity is the result of underconstrained type parametrisation. Which is why in my Haskell example code above I set the Concat a b c to (Concat a a a… so that compiler isn’t underconstrained as to which type to choose for c when the input arguments a and b are set to the same type parameter at the call site of concat a a. Yet if the programmer attempts to write code that is unconstrained by invoking/applying (aka “calling”) with concat a b then my definition of ConcatOrd a tells the compiler that a and b must be the same. Or in some cases the return type will be constrained at the call site to prevent ambiguities.

So afaics (which was @keean’s point) what this distills to is that if a programmer wants to (or unwittingly does) write underconstrained polymorphism then the capability exists in these PLs to do so. I really don’t understand how those I quoted above can claim that a ML-like module system won’t also suffer type inference ambiguities if the programmer attempts to write underconstrained polymorphic code? I understand that ML functors enable selective choice of interface(s) from signatures, but afaics as I demonstrated by example code above, so does type class inheritance. Those ML signatures and resultant ML interfaces can still be underconstrained polymorphic if the programmer so chooses. I understand (as I explained in the previous section of this comment post) that ML binds those interfaces to the object at time of construction unlike type classes which delay binding interface to objects until the call site of a function which requires such interfaces.

Thus I conclude that the cited blog is a red herring. Note that experience often trumps theory in the PL realm, so perhaps I am missing something which hasn’t been clarified sufficiently for me (and @keean) in the cited blog — which is why I discussed it with @keean given he has much more experience with Haskell and ML-like languages than my nearly nil experience with those PLs.

Navigation Menu

Repository navigation

Modularity #39

272 remaining items

Late Binding of Interface vs. Modularity?

Type Inference Issues

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Modularity #39

Description

Activity

sighoya commented on Feb 12, 2018

keean commented on Feb 12, 2018

sighoya commented on Feb 12, 2018

keean commented on Feb 12, 2018

sighoya commented on Feb 12, 2018

keean commented on Feb 12, 2018

keean commented on Feb 12, 2018

sighoya commented on Feb 12, 2018

shelby3 commented on Feb 13, 2018

keean commented on Feb 13, 2018

keean commented on Feb 13, 2018

sighoya commented on Feb 14, 2018

sighoya commented on Feb 14, 2018

keean commented on Feb 14, 2018

sighoya commented on Feb 14, 2018

272 remaining items

keean commented on Aug 15, 2018

sighoya commented on Aug 15, 2018

NodixBlockchain commented on Aug 15, 2018

shelby3 commented on Aug 15, 2018

shelby3 commented on Aug 15, 2018

shelby3 commented on Aug 16, 2018

shelby3 commented on Aug 29, 2018

shelby3 commented on Aug 30, 2018

shelby3 commented on Jan 13, 2019

shelby3 commented on Jan 13, 2019

keean commented on Jan 13, 2019

shelby3 commented on Jan 13, 2019

keean commented on Jan 13, 2019

shelby3 commented on Jan 13, 2019

shelby3 commented on Jun 10, 2020

Late Binding of Interface vs. Modularity?

Type Inference Issues

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions