Typeclass objects
Opened this issue · 302 comments
Typeclass objects offer dynamic (i.e. run-time and open modularity1) polymorphism by binding the typeclass bound to the static (compile-time) type of the reference and tagging the data type instances that the reference can contain, so that the correct dictionary can be dispatched dynamically at run-time.
They are named "trait objects" in Rust and "existential quantification" (e.g. forall a) or "existential typeclass" in Haskell.
1 Means we can't compile the universe, so we can't know all the data types required in dependency injection scenarios. Dynamic polymorphism is not just a run-time artifact, but it is also the fact of the real-world where total orders can't exist (i.e. the Second Law of Thermodynamics, Halting Problem, Incompleteness Theorem, Russell's Paradox, Byzantine Generals Problem, Byzantine fault-tolerance with CAP theorem, impossibility of existence without a quantified speed-of-light, etc). As well, there are no total orders of trustless, decentralization either.
Expression Problem
They have the benefit w.r.t. to Wadler's Expression Problem of delaying the binding of interface to data on construction of the typeclass object as opposed to OOP subclassing (and Scheme/JavaScript prototype2) which binds the interface to all instances of the subclassed type (on instantiation of the data). So they solve the Expression Problem up the point of instantiation of the typeclass object, but beyond that point while they allow adding new data types (via the aforementioned dynamic dispatch) they don't allow extending new operations after the instantation of the typeclass object which binds the allowed typeclass interface(s). Typeclass objects enable heterogeneous collections with dynamic extension of the collection of data types without requiring an invariant collections data structure (i.e. they can be the element type of an array). Whereas, typeclass bounds on function definitions delay binding the interface until the function call site and thus solve the Expression Problem up to that point, but they don't enable heterogeneous collections with dynamic extension of the collection of data types except via unions. Unions can both enable heterogeneous collections with dynamic extension of the collection of data types and delay binding of the interface until the function call site, but they require an invariant collections data structure such as a list.
2 Note that prototype programming can add new operations (but forces all instances of a prototype to take those new interfaces) and add new data types, but it can't add different interfaces to instances of the same prototype. Whereas, type classing can differentiate. (Edit: correction)
Syntax and Pecularities
Well obviously that is useless and not what I was referring to. I mean for example, I have a collection of typeclass objects and I want to sort or find them, so I need a relation.
A relation only applies to two objects of the same type.
Exactly. So thus
Eq<A, A>is useless for what I wrote above.One answer is to provide a mapping from each object type to a partial order (or total order).
So akin to subsumption to a subclass, except open to delayed definition. That might work for
sort.Or another alternative is
Eq<A, B>accepts any typeB, but always returnsfalseifBis notA. Sofindwill work.Okay I see how maybe typeclass objects are still useful. Thanks.
@keean wrote:
data Variant = for<A, B> Variant(A) requires A : Eq<B>
data Variant = Variant(A | Any) where A: Eq<Any>
That seems to be a general solution and I like it very much, unless someone can point out flaws.
So typeclass objects are always conceptually with | Any, e.g.:
let x: A where Show<A | Any> = MyType(1, 2)
let y: A where Eq<A | Any, Any> = MyType(1, 2)
Or in my (and Rust's) preferred OOPish style:
let x: A where (A | Any): Show = MyType(1, 2)
let y: A where (A | Any): Eq<Any> = MyType(1, 2)
But I prefer we can write that shorthand (and so we only need where clauses on function types and definitions):
let x: Show = MyType(1, 2)
let y: Eq<Any> = MyType(1, 2)
Hope you are also starting to see another reason why I favored an OOPish style because it is also more consistent with typeclass objects (and I actually did intuitively anticipate/expect this but not with complete solution worked out).
P.S. my understanding is that any function defined for a typeclass bound would also accept typeclass objects with that bound. The compiler would create a dynamic dispatch version of the said function on demand to be used when ever a reference to it is passed around. Seems to me that only functions called nominally can be monomorphized.
This callback can only show the type
Awhich is passed tof, the requirements should be at the top level.
f(callback: for<B> (B) => ()) where B: ShowWhere the callback can be called on any type. The first example the callback is monomorphic with respect to
f, in the second polymorphic.
I am instead proposing that be written the same as any typeclass bounded function without any for<B>:
f(callback: (B) => ()) where B: Show
I wrote in the OP:
P.S. my understanding is that any function defined for a typeclass bound would also accept typeclass objects with that bound. The compiler would create a dynamic dispatch version of the said function on demand to be used when ever a reference to it is passed around. Seems to me that only functions called nominally can be monomorphized.
This:
f(callback: (B) => ()) where B: Show
Doesn't work because you are not specifying the scope for 'B' you could mean:
for<B> f(callback: (B) => ()) where B: Show
Or you could mean:
f(callback: for<B> (B) where B: Show => ())
@keean wrote:
Doesn't work because you are not specifying the scope for
Byou could mean:
I don't understand why that is important. Please explain.
I don't understand why that is important. Please explain.
- With the
for<B>in the outer scope the callback is monomorphic with respect tofso the callback can only be called on one type, that is fixed at the timefis called. - With the for in the inner score we are passing a polymorphic function that can be called on any
B
@keean wrote:
- With the
for<B>in the outer scope the callback is monomorphic with respect tofso the callback can only be called on one type, that is fixed at the time f is called.
Okay what you mean is that when f is called, then at the call site the types of the callback are monomorphized. This means f is only calling the callback with the said typeclass bounded instances and not with concrete data instances.
I don't think the for<B> is necessary. The scope can be determined by whether the where clause appears at the top-level scope or not! So non-top-level indicates a typeclass object; whereas, top-level indicates monomorphization at the call-site of f. So now, you provided another more important reason that we need non-top-level where clauses. I hate that ugly/noisy for<B>.
- With the for in the inner score we are passing a polymorphic function that can be called on any
B
Right that is what I wrote else where, that it doesn't make any sense for f to request a typeclass bounded callback (which isn't monomorphized at the call site for f) unless it is for dynamic dispatch typeclass object(s).
Yes but I would rather make the programmer declare a datatype for a polymorphic callback function. This keeps the function syntax simpler, and is called first-class-polymorphism.
I think its a bit more of a problem. Its not the typeclass object that is needed. Consider:
f(callback : MyCallbackFn) where ...We want to create the where clause when declaring
fbut we don't yet know the callback function that will be passed. We don't know what typeclass bounds the callback will have.If we want the callback to print it may need a
Showconstraint, we cannot know at the pointfis declared what typeclass bounds callback will have, and to define them would be to restrict what the callback is allowed to do, which does not seem right.
I am pleased you raised this point.
First re-read my prior comment and click the link in it to remember what you pointed out to me about the scoping of the callback.
If the callback is scoped by the call site to function f, then the caller chooses the typeclass bound(s), which satisfies your point.
And if the callback is scoped by the function f, then f decides the typeclass bound(s) of the typeclass object(s) of the callback.
What needs to happen is we need to infer the typeclass bounds on
fwhenfis called with a specific callback which has known typeclass bounds.I think the callback example needs type-class bounds inference at the callsite of
fin order to be useful.
If you are not referring to augmentation of type-class bounds, that would only be in the case when the callback is scoped by the call-site of f, except it is generally impossible. Let's clarify what kind of inference we are taking about.
The function f may call some operations on the callback and/or it may store f in a data structure imperatively and thus we have no way of knowing which future operations on the callback will be allowed if f does not declare them. The compiler will force f to declare them. You could I suppose infer the operations that f internally requires in its function body using principal typings, but we don't know yet to what extent we can support principal typings, as generally they are undecidable in an open system.
So f probably must declare its typeclass bound(s) requirements (at least we decided at a minimum, it must be explicit at module boundaries).
If we want the callback to print it may need a
Showconstraint, we cannot know at the pointfis declared what typeclass bounds callback will have, and to define them would be to restrict what the callback is allowed to do, which does not seem right.
But you are making a different point. You are talking about the caller of f being able to augment (not remove the typeclass bounds f requires) the available typeclass bounds that the callback requires in the case where the callback is scoped at the call-site of f. In this case, I agree with you, since you want to delay unification of the type variables until the call-site.
So what you are saying is that f can require operations on the type variables of the callback and the caller can add some more required operations.
The caller can add more where requirements (either inferred or explicit) at the call site of f. The way the explicit will be done at call site is with a cast either top-level:
f(callback): (MyCallback) => () [B: Print+Show]
Or non-top-level:
f(callback: (B) => () [B: Print+Show])
Note above that either will apply to the typeclass object or monomorphization cases, because per my proposal, f's scoping of its where clause determines which case it is.
@keean wrote:
Yes but I would rather make the programmer declare a datatype for a polymorphic callback function. This keeps the function syntax simpler, and is called first-class-polymorphism.
But that forces structural typing otherwise we can't reuse functions which have the same signature but different data type names. That is why I had suggested type aliases instead.
And type aliases must be expandable to any general types, so we won't be able to force (make) the programmer use type aliases for non-top-level where clauses (as they can use the general types any where a type signature is required).
Edit: more discussion.
@keean wrote:
By using first class polymorphism we can assume all function signatures are monomorphic which avoids the need to keep track of the nesting where type variables are brought into scope
Can you please provide an example or more detailed explanation so I can grok this? (Also for readers' benefit)
, and allows us to standardise on a single top level
whereclause for all datatypes and function definitions. We can still construct arbitrary higher ranked types by using datatypes.See this paper, I think it explains it quite well. http://web.cecs.pdx.edu/~mpj/pubs/fcp.html
However I think we should use first class polymorphism so we don't have such complex function signatures. With first class polymorphism we can declare a data-type:
data MyCallback = (B) => () requires B : Show f(callback : MyCallback)Please show me example syntax for instantiating an instance of
MyCallback?Shouldn't that be instead:
data MyCallback = MyCallback((B) => () requires B : Show)Yes, you are right, we require the constructor for the type to have
()brackets. Basically it would be the normal monomorphic function declaration inside a datatype, and any type variable that is free on the right hand side gets automatically universally quantified.As the paper says, it keeps the syntax simpler, is easier to implement, but has the same expressive power as free annotation of functions. I think it will make for cleaner APIs too, as you can use the named type to give check you have the right type for your callback (so less typing when using libraries).
Okay so the research paper you cited is all about achieving type inference.
So as I wrote in my prior comment in this thread, you are advocating abandoning the ability to reuse functions (which contain a type variable) based on their structural type and instead forcing said functions to be instantiated nominally (thus making equivalent structural function types non-composable because they have different nominal constructors), all because you want to be able use principal typings on these said functions. I've already warned and feared that you are going to making your principal typings goal into a weapon to defeat degrees-of-freedom of expression. @skaller has also warned similarly that type inference is the enemy of expressiveness.
I don't think it is often going to be the case that we want to have a function taking a callback, where both said function and the callback function are both not annotated with quantified (aka concrete) types. And for those cases where might have wanted to do that, we won't. We will have to annotate. For myself and also for readers, please provide me a convincing example showing this annotation overhead (in this specific case of type variables we are discussing) is a significant burden justifying abandoning the ability to compose functions generally?
Edit: also nothing stops you from using the method you prefer in your code and achieving type infererence. I am asking why we must force everyone to abandon function composition generality in all code, when they can choose to annotate.
I don't think I like complex code without type annotations. Raises cognitive load due to lack of explicit local reasoning. Type inference is useful where the reader can easily figure out in their head what the type annotations would have been. This is one of my big complaints that makes Haskell code so obtuse to read IMO.
I don't think it is often going to be the case that we want to have a function taking a callback, where both said function and the callback function are both not annotated with quantified (aka concrete) types. And for those cases where might have wanted to do that, we won't. We will have to annotate. For myself and also for readers, please provide me a convincing example showing this annotation overhead (in this specific case of type variables we are discussing) is a significant burden justifying abandoning the ability to compose functions generally?
There is no loss in expressive power (it even says so in the paper), and it will make the type signatures shorter and more readable.
There is no loss in composition, and I am not sure why you would suggest there is? Function type signatures don't compose, unless you are talking about copy-and-paste composition? Copy-and-paste just leads to stupid errors. Why bother with named functions at all, why not just copy and paste the raw-code? The same argument applies to types, it is better to have a named type you can re-use (like you call functions) rather than have people copy-and-paste huge complex and unintelligible type signatures.
Okay so the research paper you cited is all about achieving type inference.
I disagree, it is all about avoiding having to have higher ranked type annotations. In Haskell (and all other languages I know of except those that use FCP) you must annotate higher ranked types because they cannot be inferred. Haskell cannot infer them, no language I know of can infer them. So this is not about inference. This is about how you achieve the annotation. We already need first-class-polymorphism to correctly handle type-class dictionaries, so we already will have the mechanism for it.
We can keep the language simpler and keep the full expressive power, how could anyone not want that?
@keean wrote:
There is no loss in expressive power (it even says so in the paper),
I guess that is correct. I think I also used the term 'composition' and so it is really boilerplate that is the issue.
and it will make the type signatures shorter and more readable.
At the cost of causing other boilerplate...
There is no loss in composition, and I am not sure why you would suggest there is?
I can't reuse a MyCallback every where I can use a MyCallback2 (and vice versa) even if the signature of the functions are otherwise identical.
Granted I can destructure those constructors and re-construct a compatible instance, but this is boilerplate and additionally afaics if I have these in a typeclass object, then I will have need a different implementation for each one. Afaics, FCP is increasing boilerplate of composition in exchange for the hope of not having to write type annotations for higher-ranked types (and I say hope because I don't know if FCP inference will integrate with our unions and other features and I don't know if we won't end up needing higher-ranked types any way).
I disagree, it is all about avoiding having to have higher ranked type annotations.
Which is precisely all about achieving (a similar level of expressiveness with) type inference. But the entire point of type inference is to not have boilerplate. I hope you didn't really expect that FCP is some Holy Grail without trade-offs.
So this is not about inference. This is about how you achieve the annotation.
It is about how we support type variables with minimal annotation and boilerplate, with the goal of enabling type inference with a boilerplate wrapping versus losing type inference with no boilerplate wrapping.
We can keep the language simpler and keep the full expressive power, how could anyone not want that?
How is it simpler? You trade off one thing for another.
The same argument applies to types, it is better to have a named type you can re-use (like you call functions) rather than have people copy-and-paste huge complex and unintelligible type signatures.
The difference is we don't normally expect structurally equivalent types to be equivalent (excluding our planned unions and intersections). But functions we normally do expect them to be composable on structurally equivalence (which is why we allow anonymous functions).
Note you did not address my comment here:
@shelby3 wrote:
Edit: also nothing stops you from using the method you prefer in your code and achieving type infererence. I am asking why we must force everyone to abandon function composition generality in all code, when they can choose to annotate.
How is it simpler? You trade off one thing for another.
You avoid nested where clauses in the syntax. The grammar will be simpler, (and this will be visible in the simple EBNF for the language).
The difference is we don't normally expect structurally equivalent types to be equivalent. But functions we normally do expect them to be composable on structurally equivalence.
We dont normally expect any equivalence operator to work on functions, so I am not sure this is important. Remember top-level functions can be fully polymorphic, so you only need to wrap the argument in the datatype at the call site. Like this:
data MyCallback = MyCallback((A) => A)
id(x : A) : A => x
fn(callback : MyCallback)
fn(MyCallback(id))
What is wrong with type annotations?
They’re great! They add to the ability to reason about code in principle.
They allow error messages to make sense.
The downside of annotation is verbosity which makes code harder to read.
The programmer should have flexibility chosing the tradeoff.
—
john skaller
skaller@users.sourceforge.net
http://felix-lang.org
@keean wrote:
We dont normally expect any equivalence operator to work on functions, so I am not sure this is important.
Disagree. We expect assignment of functions to work on structural equivalence.
fn(MyCallback(id))
And so you are right back to type annotations again.
How is it simpler? You trade off one thing for another.
You avoid nested
whereclauses in the syntax. The grammar will be simpler, (and this will be visible in the simple EBNF for the language).
We avoid that but add the boilerplate back in other places. So isn't necessarily a net gain in brevity. It also loses some local reasoning.
The nested where clauses can be avoided without forcing FCP, by offering a type alias as I mentioned twice before.
And you didn't address my comment:
@shelby3 wrote:
and additionally afaics if I have these in a typeclass object, then I will have need a different implementation for each one
Generally wrapping interacts badly because it becomes deeply nested!!!
Which is why we want a first-class anonymous union instead of massive case-tree logic to destructure Either. OTOH, first-class without wrapping makes inference undecidable.
Edit: also nothing stops you from using the method you prefer in your code and achieving type infererence. I am asking why we must force everyone to abandon function composition generality in all code, when they can choose to annotate.
Because it adds complexity to the implementation and the grammar, and complexity is the enemy of good software. Expressive power is achieving the most with the least.
What is wrong with type annotations?
Nothing is wrong with writing types, but the more complex the nesting of types, especially higher-ranked types is confusing. If we are aiming to make this easy for people coming from OO to pick up then we will want to make the type signatures as easy to understand as possible.
As I said above, this has nothing to do with inference, you have to write the types in either case, but the main difference is that with FCP all the quantifiers are implicit and all the where clauses are at the top level, simplifying the syntax, for no loss in expressive power. It makes the code cleaner and easier to read.
and additionally afaics if I have these in a typeclass object, then I will have need a different implementation for each one
No a single record or typeclass object encapsulates all the polymorphic functions so you do not need this.
For example:
data MyCallback = MyCallback {
fna (A -> A) : A
fnb (A -> A -> A) : A
}
Works exactly the same as the single argument tuple datatype posted before.
Generally wrapping interacts badly, which is why we want a first-class anonymous union instead of massive case-tree logic to destructure Either. OTOH, first-class without wrapping makes inference undecidable.
It has nothing to do with inference as you have to provide the type signature in either case, it is just where and how that signature is written that changes. FCP uses the same mechanism as type-class dictionaries.
We avoid that but add the boilerplate back in other places. So isn't necessarily a net gain in brevity. It also loses some local reasoning.
Callbacks are not local in any case, as the callback could happen from anywhere. Consider async-IO, you call write with a callback, and flow immediately continues with the next statement. The callback will be called by some non-local code in the IO complete event handler. In JavaScript this can only happen after the current "program" has finished returning control to the main event-loop.
Readers to understand what we are discussing now, I think it is helpful to understand this way of emulating higher-ranked types which I was introduced to me at the Rust language forum:
trait Foo {
fn call<A: Read>(&self, a: A);
}
fn f<G: Foo>(g: G, pred: bool) {
if pred {
g.call(File::open("foo").unwrap());
} else {
g.call(Cursor::new(b"foo"));
}
}By giving a name Foo to the type constructor for the function call, we are able to delay quantification of type variable <A: Read> until the body of the function f. Compare that to the example which failed to compile:
fn f<A: Read, G: Fn(A) -> ()>(g: G, pred: bool) {
if pred {
g(File::open("foo").unwrap());
} else {
g(Cursor::new(b"foo"));
}
}The above won't compile without higher-ranked types (which Rust doesn't support), because the quantification of <A: Read> is at the call-site for function f. So even if we did not place the : Read bound on A, the inference engine could not infer the correct type for A, which happens to be an intersection of two quantified functions where A is a File or a Cursor.
In general, inference of function application over unions and intersections diverges into infinite recursion in the inference and is undecidable. @keean showed me an example of that using expansion variables in private discussions last May. The two higher-order features are like mirrors facing each other, thus enabling mutual recursion.
Generally wrapping interacts badly because it becomes deeply nested!!!
It is still better than the alternative of a huge multi-line type signature all in one block.
@shelby3 looking at the direction you want to go, we may be better off ditching quantified types and type-classes altogether and going for a full intersection and union type system with ad-hoc overloading?
@keean wrote:
Generally wrapping interacts badly because it becomes deeply nested!!!
It is still better than the alternative of a huge multi-line type signature all in one block.
Disagree! The deep nesting totally breaks any reasonable composition.
Also we don't need to force FCP in order to get type aliases:
@shelby3 wrote:
The nested
whereclauses can be avoided without forcing FCP, by offering atypealias as I mentioned twice before.
@shelby3 I feel you are making statements about a style you have no experience of coding, so I am not sure how much weight to give your objections.
I haven't made any decision. I am trying to analyze the trade-offs.
Intersection types allow functions to be like a type-class where a single function can have different signature that apply to different types. You no longer need the boilerplate of declaring a type-class you just define two functions with different type signatures that have the same name.
@keean wrote:
and additionally afaics if I have these in a typeclass object, then I will have need a different implementation for each one
No a single record or typeclass object encapsulates all the polymorphic functions so you do not need this.
You misunderstood. The context of my point was MyCallback and MyCallback2 both having the same structural type, but requiring separate implementations for a typeclass bound, because they have different (nominal) types.
And then factor in deep nesting and you are in implementation proliferation hell.
The context of my point was MyCallback and MyCallback2 both having the same structural type
Why would you declare two of them then? Thats like saying add and add2 both have different names despite both adding numbers exactly the same way. You don't need someone to stop you defining the add function more than once, why would you need someone to stop you defining "MyCallback" more than once. Its something you just wouldn't do.
As I said above, this has nothing to do with inference, you have to write the types in either case, but the main difference is that with FCP all the quantifiers are implicit and all the where clauses are at the top level, simplifying the syntax, for no loss in expressive power. It makes the code cleaner and easier to read.
Implicit quantifiers do NOT make code easier to read. Its like most “simplifications”,
they seem like a good idea at the time, they work well for simple cases,
but its a disaster precisely in the cases where you think it would serve best,
the complex cases.
Its a known fact that human information transmission requires redundancy.
Perhaps less for smarter people, or people familiar with the domain,
more for others. But for language, psychologists have actually MEASURED
the amount of redundancy that gives the best comprehension, its somewhere
between 15 and 30% I believe (in linear text).
Computer programming languages may require different redundancy.
but infering types everywhere clearly defeats the whole point of having
type annotations: to provide redundant information for validation and
confirmation.
—
john skaller
skaller@users.sourceforge.net
http://felix-lang.org
@keean wrote:
The context of my point was MyCallback and MyCallback2 both having the same structural type
Why would you declare two of them then? Thats like saying add and add2 both have different names despite both adding numbers exactly the same way.
You have this big blind spot that repeats over and over even though I've mentioned to you 5 or more times that total orders don't exist in our universe.
In open modularity, you can't control the proliferation of duplication. It is impossible to maintain tight control over anything in a decentralized context.
You have this big blind spot that repeats over and over even though I've mentioned to you 5 or more times that total orders don't exist in our universe.
If it is not a problem for named functions, it is not a problem for named types either.
Computer programming languages may require different redundancy.
but infering types everywhere clearly defeats the whole point of having
type annotations: to provide redundant information for validation and
confirmation.
What I know from experience is that a complete absence of types in code makes local reasoning harder and is a problem.
What I also know is that requiring explicit types everywhere is excessive boilerplate that gets in the way of what the code is actually doing.
So I think the sensible answer is somewhere in the middle, that types need annotating in some situations but not others. In order to minimise the cognitive load of understanding where annotation is necessary, the rules must be simple, generic, and easily applicable.
@keean wrote:
You have this big blind spot that repeats over and over even though I've mentioned to you 5 or more times that total orders don't exist in our universe.
If it is not a problem for named functions, it is not a problem for named types either.
I already argued to you why afaics that isn't normally the case:
@shelby3 wrote:
The difference is we don't normally expect structurally equivalent [nominal] types to be equivalent. But functions we normally do expect them to be composable on structurally equivalence.
We don't usually compose over the structure of nominal type constructors (and we can pattern match destructure when we need to). That is why we choose a nominal type system. But we don't normally choose a nominal typing system for functions, because we tend to want to deeply nested compose on the structure of functions.
I think perhaps this is because types other than functions are encouraged to be composed via operations, whereas functions are operations. It seems functions are the fundamental building block.
@shelby3 If we are agreed that we can imply polymorphism in datatypes in exactly the same way we do in function signatures, in other words:
(A) => A
is a generic function over all A`s, so these are different:
data T<A> = T(A) // parametric type
data T = T(A) // universally quantified type
Then I am happy to leave the decision on what to do with function type signatures to you, although we probably need to discuss the syntax further if we are going to have higher ranked types directly in function type signatures.
@keean wrote:
Edit: also nothing stops you from using the method you prefer in your code and achieving type infererence. I am asking why we must force everyone to abandon function composition generality in all code, when they can choose to annotate.
Because it adds complexity to the implementation and the grammar, and complexity is the enemy of good software. Expressive power is achieving the most with the least.
I don't yet understand the scenarios where if we don't support higher-ranked types, then where with annotations we can't do something we need to do w.r.t. to where clauses not all at top-level, without resorting to wrapping in FCP??
Can you help me better understand? That FCP paper is too dense for me to translate quickly into examples and syntax I readily grok (and I am lacking time/energy).
@keean wrote:
We avoid that but add the boilerplate back in other places. So isn't necessarily a net gain in brevity. It also loses some local reasoning.
Callbacks are not local in any case, as the callback could happen from anywhere
You are conflating type (which would be local) with definition and invocation of the callback.
Can you help me better understand? That FCP paper is too dense for me to translate quickly into examples and syntax I readily grok.
With FCP once the generic function is wrapped, it can be treated as a normal generic type, so for example:
id(myCallback)
The type of id remains (A) => A and yet myCallback with all its internal polymorphism and constraints behaves like any other first class value. Thats why it is called first class polymorphism.
You would have to construct special identity functions (and other generic functions) for each different higher-ranked type you wanted to deal with.
@keean wrote:
OTOH, first-class without wrapping makes inference undecidable.
It has nothing to do with inference as you have to provide the type signature in either case
Well yeah that is my point! But your cited paper claims otherwise:
We have described a modest extension of the HindleyMilner type system that offers both the convenience of type inference and the expressiveness of first-class polymorphism
On 10 Oct 2016, at 05:54, Keean Schupke notifications@github.com wrote:
So I think the sensible answer is somewhere in the middle, that types need annotating in some situations but not others. In order to minimise the cognitive load of understanding where annotation is necessary, the rules must be simple, generic, and easily applicable.
I agree. And the sensible middle ground is to allow type annotations to be omitted where they can be calculated bottom up,
that is, entirely locally, with reference of names to surrounding context.
This means to me HM-inference is on the wrong side of the division because the types are calculated from unnamed usage. It also means overloading is suspect because you cannot be certain when you lookup a name you have found the complete overload set: type classes are a compromise here (the function is the class is unique, the instances are not, so the problem is reduced by splitting it into two parts).
This general argument applies to syntax too. (x) => (x) is worse than \x -> x because the \ announces a function, whereas ( may or may not, depending on context:
(x) => (x) => (x)
Woops! You didn’t see that second => before did you! Whereas this is even clearer but more verbose:
fun (x) => fun (x) => x
—
john skaller
skaller@users.sourceforge.net
http://felix-lang.org
@keean wrote:
looking at the direction you want to go, we may be better off ditching quantified types and type-classes altogether and going for a full intersection and union type system with ad-hoc overloading?
I haven't made any decision. I am trying to analyze the trade-offs.
Intersection types allow functions to be like a type-class where a single function can have different signature that apply to different types. You no longer need the boilerplate of declaring a type-class you just define two functions with different type signatures that have the same name.
You used to mention this to me in private discussion and I think I had explained that this breaks the Expression Problem solution, because we can't add new data types independently of new operations.
The selection of a typeclass dictionary enables the data types and the functions which consume the dictionaries to varying orthogonally.
This means to me HM-inference is on the wrong side of the division because the types are calculated from unnamed usage. It also means overloading is suspect because you cannot be certain when you lookup a name you have found the complete overload set: type classes are a compromise here (the function is the class is unique, the instances are not, so the problem is reduced by splitting it into two parts).
The algorithm I am using is compositional, that means it only uses local information, and typed program fragments are composable - there value part composes, and the type part composes separately.
I think the biggest advantage of FCP is that generic templates can be treated as ordinary values, which makes them first class entities in the language.
@shelby3 wrote:
The difference is we don't normally expect structurally equivalent [nominal] types to be equivalent. But functions we normally do expect them to be composable on structurally equivalence.
We don't usually compose over the structure of nominal type constructors. That is why we choose a nominal type system. But we don't normally choose a nominal typing system for functions, because we tend to want to compose on the structure of functions.
I think perhaps this is because types other than functions are encouraged to be composed via operations, whereas functions are operations. It seems functions are the fundamental building block.
I agree in principle, however, there are SOME data types we want structural: tuples and records and arrays.
Also, less common, unit sums.
Felix has structural variants, Ocaml polymorphic variants are partially structural,
but normally we use nominal types for variants.
Nominally typed products are most useful for abstractions.
However languages like C++ are absurd because all products have
to be nominally typed except arrays.
Pointers are a good example of where nominal typing would be complete madness.
—
john skaller
skaller@users.sourceforge.net
http://felix-lang.org
@keean wrote:
Can you help me better understand? That FCP paper is too dense for me to translate quickly into examples and syntax I readily grok.
With FCP once the generic function is wrapped, it can be treated as a normal generic type, so for example:
id(myCallback)The type of
idremains(A) => Aand yetmyCallbackwith all its internal polymorphism and constraints behaves like any other first class value. Thats why it is called first class polymorphism.
But unless id needs higher-ranked types, then it has specified the typeclass bounds on its signature, so there is no need to hide myCallback's internal type variables (to simulate higher-ranked types), because they are all quantified by id's signature.
So I am failing to see any advantage in simplicity for FCP unless we need higher-ranked types. Am I incorrect?
You would have to construct special identity functions (and other generic functions) for each different higher-ranked type you wanted to deal with
But what if we don't need higher-ranked types?
But what if we don't need higher-ranked types?
You need higher ranked types when you want to pass a "generic function" as an argument. Without higher-ranked-types you can only pass concrete functions with known types as arguments into functions.
@keean wrote:
But what if we don't need higher-ranked types?
You need higher ranked types when you want to pass a "generic function" as an argument. Without higher-ranked-types you can only pass concrete functions with known types as arguments into functions.
Did you forget that I proposed that non-top-level where clauses on function definitions of callback arguments, would indicate a typeclass object. Thus there isn't any "generic function" (for monomorphization) being input, as it is dynamic polymorphism (one function for all dynamic types).
Afaics, I have nothing against using FCP for emulating higher-ranked types.
Did you forget that I proposed that non-top-level where clauses on function definitions of callback arguments, would indicate a typeclass object. Thus there isn't any "generic function" (monomorphization) being input, as it is dynamic polymorphism (one function for all dynamic types).
"type-class objects" have a higher-ranked-type.
"type-class objects" have a higher-ranked-type.
Huh? Example please. I am thinking that the typeclass bound is specified by the function id and so all use of the callback within the body of id is using those statically declared bounds.
@shelby3 wrote:
"type-class objects" have a higher-ranked-type.
Huh? Example please. I am thinking that the typeclass bound is specified by the function
idand so all use of the callback within the body ofidis using those statically declared bounds.
The typeclass bounds are the nominal lifting to emulate the higher-ranked aspect of typeclass objects. You don't need another redundant wrapping data on the function that has typeclass objects.
The typeclass bounds are the nominal lifting to emulate the higher-ranked aspect of typeclass objects. You don't need another redundant wrapping data on the function that has typeclass objects.
A "typeclass-object" type would look like this:
data MyObject = for<A> MyObject(A) requires Show A
@shelby3 This is not about syntax, it is about what a typeclass-object actually is. You can call it whatever you like and have whatever syntax you like, it does not change what its type is, which I wrote above using something like the syntax we agreed.
A typeclass-object is an existentially quantified type, this means it has a local type variable introduced bu the existential quantifier. We can perform a well known transformation to turn the existential quantifier into a universal quantifier. So a typeclass-object is a parameterised type where the type variable is introduced in the outer-most-scope (of the typeclass-object type) by a universal quantifier, and constrained by any typeclass constraints we require.
Changing the syntax does not change the fundamental nature of the type.
@shelby3 I am happy to have higher ranked types and first class polymorphism if you want, but I think we only need first class polymorphism. I would suggest we keep to one if possible (which I think has to be FCP) to keep the language simple.
@keean wrote:
This is not about syntax, it is about what a typeclass-object actually is. You can call it whatever you like and have whatever syntax you like, it does not change what its type is
Agreed. That is my point also. I think you are conflating and don't understand the type of the typeclass object and how it applies to our discussion. But maybe I am incorrect, so please help me to clarify as follows.
A typeclass-object is an existentially quantified type, this means it has a local type variable introduced by the existential quantifier. We can perform a well known transformation to turn the existential quantifier into a universal quantifier. So a typeclass-object is a parameterised type where the type variable is introduced in the outer-most-scope (of the typeclass-object type) by a universal quantifier, and constrained by any typeclass constraints we require.
I noted your example downthread.
So for readers' benefit and also to make sure I have the same understanding as you, "existentially quantified type" means that by declaring that the type of the typeclass object exists with static typeclass bounds, then the typeclass bounds are not variable (i.e. it is not a universally quantified type). And it has a "local type variable" (which is actually Any or the Top type because it is never quantified at compile-time) which allows a reference to an instance of the typeclass object to contain any data type which implements the "existentially quantified type" typeclass bounds. Afaik, in general existential types can be bounded by concrete types as well, not just typeclass bounds although that does not apply in the context of a typeclass objects.
And my point is that above is analogous to the equivalent simulation of a higher-ranked type in that the typeclass bounds operations are employed within the consuming function on any polymorphic type (which is the said local variable). Which I also mentioned in another comment.
So there is no need to wrap a function containing typeclass objects, because that local variable is dynamic polymorphism and is always Any (Top) at compile-time (and that is why it must be local!).
We can perform a well known transformation to turn the existential quantifier into a universal quantifier.
I already explained that at the call-site we can't remove or change the typeclass bounds of a typeclass object, rather can only augment them. Because any operations the function that is consuming the callback relies on, can't be removed.
It seems you must be referring to augmenting the typeclass bounds of the typeclass object at function defintion site that has deeply nested functions which take callbacks, and that top-level function wants to augment the typeclass bounds of the callbacks. I don't disagree with this, but afaics this is not requiring higher-ranked types (Edit: see later comments which analyze monomorphization). So it seems you are conflating two separate concepts.
You seem to be conflating the need to augment the typeclass bounds at the top-level scope with the need for wrapping for higher-ranked types.
I just don't see where we need higher-ranking typing for typeclass objects. I asked you to please provide an example if you think otherwise.
@keean wrote:
I am happy to have higher ranked types and first class polymorphism if you want, but I think we only need first class polymorphism.
Did you not grok the significance of what I quipped?
@shelby3 wrote:
Afaics, I have nothing against using FCP for emulating higher-ranked types!
I do not (yet) see any dire need for adding higher-ranked typing, when it can simulated with FCP. So we are in agreement.
But I also don't see why we need to use FCP for declarations of typeclass objects in callbacks, because afaics those are not otherwise requiring higher-ranked typing. It seems to me you are conflating the need for augmenting typeclass bounds in the outer scope with higher-ranked typing.
My understanding is that higher-ranked typing is where we have some type variable at function signature scope that we want to track through the body of the function and infer all the operations required on that type variable, rather than explicitly annotating the types.
Thus if we are declaring all the typeclass bounds in the where clause, then we have annotated the types. So how can that be higher-ranked?
To expound on my prior comment, higher-ranked types are where we want to pass around functions that have type variables as first-class values:
https://www.stephanboyer.com/post/115/higher-rank-and-higher-kinded-types
http://stackoverflow.com/questions/13317768/kind-vs-rank-in-type-theory
And this reinforces my point, which is that whether we augment or not type-class bounds at the top-level for function definitions containing nested callbacks with typeclass object types, is not causing functions with type variables to be passed as first class values, because the static type is the existentially quantified as the static typeclass bounds. The polymorphism is dynamic at run-time, not static at compile-time.
On 10 Oct 2016, at 20:47, shelby3 notifications@github.com wrote:
My understanding is that higher-ranked typing is where we have some type variable at function signature scope that we want to track through the body of the function and infer all the operations required on that type variable, rather than explicitly annotating the types.
So called “higher ranked types” are ones which have quantifiers in positions
other than the head of the type.
In logic:
-
Predicates can be calculated entirely with truth tables. This is zero’th order logic.
-
First order logic allows quantifiers followed by a predicate for example
for all x , for all y, P (x,y)
-
Second order logic allows quantifiers inside the formula
for all x, (for all y there exists a z such that x < z < y)
This corresponds, by the Curry Howard isomorphism, to types:
- primtive types int, float, string are zero’th order
- first order types like for all t, list t.
- second order types like int -> (for all x. x -> string) -> bool
which is the type of a function accepting an int, returning a function
that accepts a polymorphic function that converts any type to a string,
and returns a bool.
That’s a “higher ranked type”. An example of the use in Ocaml:
let f (g: ‘a. ‘a -> string) (x:int) (y:float) =
print_endline (g x);
print_endline (g y)
in
So the g passed in is polymorphic. The ocaml notation
‘a . ‘a -> string
is read
“for all alpha, a function accepting alpha and returning string”
Now as you can see, this function takes polymorphic g as a parameter.
Which means at run time, g has to be polymorphic. This is not so easy!
Sometimes, you want to use a type class for g instead. That helps
because you get two different instances of g. So there’s no second
order polymorphism.
But of course there would be if you wanted function “f” to be in a type
class. And you can also have higher order data types.
higher order things are hard becaue you cannot monomorphise them.
First order polymorphism can always be monorphised away.
By the way this is confusing but:
for all T. list[T]
is an indexed family of types. But
list
is a data functor. It is not a type. It is a type function:
TYPE -> TYPE
which given any type (such as int) produces another type,
such as list[int]. It is quite confusing!
—
john skaller
skaller@users.sourceforge.net
http://felix-lang.org
On 10 Oct 2016, at 21:34, shelby3 notifications@github.com wrote:
To expound on my prior comment, higher-ranked types are where we want to pass around functions that have type variables as first-class values:
That’s one way to do it.
Most functional programming languages do not do that.
They use boxing instead.
—
john skaller
skaller@users.sourceforge.net
http://felix-lang.org
So let me try to recap where I think we are on this issue, so hopefully we can reach some consensus and move forward.
Since I thought we would not have higher-ranked typing (notwithstanding that we will probably support the FCP nominal type constructor wrapping for simulating some of the expressiveness of higher-ranked typing), then I presumed when accepting parametric functions (i.e. those with type variables) as first-class values (e.g. as callbacks), then these type variables would always be:
- bounded by typeclass
- fully quantified at either the function definition site or the call-site
- any quantification at the top-level (either at definition or call-site) would augment existing bounds
I can't see how that is higher-ranked (unless we are referring to the ability to monomorphize, see below...). Even if we elide the typeclass anotations and wish to infer them, the inference is deductive from the bottom-up since we look for the operations that each function body requires which dictate which inferred typeclass bounds provide those operations.
Thus afaics, the issue of whether we place where clauses at the top-level or optionally also at the inner nesting levels for arguments, is not related to higher-ranked typing and FCP (again unless we are referring to the ability to monomorphize, see below...).
I also noted that the compiler can't monomorphize functions which are passed around by typed reference (instead of by name) because (absent higher-ranked typing) we only have one pointer (in the reference) back to the body of the function so the compiler can't create ex post facto (after the assignment of the nominal to a reference type) numerous variants needed to monomorphize. Thus if we pass a callback by reference instead of by name, then said callback must employ typeclass objects instead of monomorphized typeclass bounds. I had proposed that non-top-level where clauses would dictate that a typeclass object was required, but now due to my prior sentence, I realize that the call-site can determine if the function requires a typeclass object, not the function definition. Thus I rescind my assertion of that being a justification for a requirement for needing non-top-level where clauses.
In the context of the compiler being able to do monomorphization of the callback function when we pass it by name (instead of by reference), a named function in that context seems to be analogous to FCP.
One thing I think I am noticing if I am not mistaken is that the declaration of whether a function is using typeclass objects should not occur at the function definition site, but rather at the use (call) site. Afaics, the compiler can automatically generate a typeclass objects variant of any function that has typeclass bounds. Thus it is the call-site and assignment site which determines whether a function is using typeclass objects or monomorphization. When a function is assigned to a typed reference (i.e. is no longer referenced nominally), then the compiler can no longer monomorphize it, thus it must be a typeclass objects variant. And when passing typeclass object instances to a function at the call-site, then a variant of the function which accepts typeclass objects must be employed by the compiler.
So if my prior comment was correct, then I see no need to wrap function types in data constructors. The call-site can determine whether ("higher-ranked") monomorphization or typeclass object is employed.
However, I did realize just now that the function definition site may need to declare that it requires a typeclass object for an argument of a callback, if it is calling the callback passing a typeclass object (and it may wish to make this declaration for specific arguments of the callback, not necessarily all of them). But if we are monomorphizing then it means the body of the function invoking the callback is going to be analyzed any way in order to know which data types to monomorphize, so it seems the explicit declaration for a typeclass object is again not required.
I am failing to understand how passing around a data MyCallback type could ever be monomorphized in general? The function inputting the callback may call other functions passing the same callback, which may call other functions, recursively. Do we monomorphize turtles all the way down? Wouldn't that be dependent typing?
@skaller wrote:
higher order things are hard becaue you cannot monomorphise them.
Isn't monomorphization for first-class (second-order) polymorphism inherently undecidable?
So if I don't have mistakes in my thought process today, I am thinking that often we will be forced to use typeclass objects for functions as first-class values having typeclass bounds.
One more point which I touched on before but may have not incorporated into my recent comments. The call-site for a function taking, or even the definition site taking a nested function which takes, a callback may want to augment the typeclass bounds required for the callback. But this can only be done if the call will be monomorphized, which in general can't always be done.
One possible reason to want where type bounds clauses on non-top-level function arguments (i.e. for callbacks), is so for example we can specify at the call-site the free (those not associated with arguments) type variables with the <...> on the callback argument instead of on the top level function call, although I guess it would be possible to place the <...> for those on the function type argument in the definition.
Again as I wrote before, for abbreviation of non-top-level types (including those when a where clause) a type alias could also be considered.
What concerns me overall is how complex this is becoming. I'd prefer to find some simplification.
@shelby3 wrote:
What concerns me overall is how complex this is becoming. I'd prefer to find some simplification.
And what I am thinking is I may want to forsake monomorphization of callbacks, i.e. all first-class (second-order) polymorphism will be dynamic dispatch with typeclass objects. There will also be unions if need to keep the Expression Problem solution open for first-class functions. I don't want to abandon monomorphization of typeclass bounds for all arguments in function calls, just for the callbacks in those.
The monomorphization of first-class (second-order) polymorphism seems special case prone and obtuse. Yet I am waiting on feedback.
How much have you used FCP with typeclass bounded callbacks in your code? Why was it necessary?
Not a lot, because only rarely do you need runtime polymorphism. Compiler abstract syntax trees are one of the classic examples where it is necessary, so I am sure we will get plenty of opportunity to see if we have it covered in our implementation.
Writing a traverse function that descends the tree calling a polymorphic callback on each node would be a good example.
@keean wrote:
Not a lot, because only rarely do you need runtime polymorphism.
So if you acknowledge FCP requires runtime polymorphism, why not use typeclass objects?
Writing a traverse function that descends the tree calling a polymorphic callback on each node would be a good example.
Wouldn't typeclass objects accomplish that?
Or a union of all the types in the tree.
Seems that is precisely the need for the union so it remains open to new operations, which was my point about how it solves the Expression Problem.
How FCP will help if typeclass objects don't? Still need to know all the data types in the tree, else you can't apply new polymorphic operations.
There is another circumstance where FCP us useful without runtime polymorphism, and that is where you wish to statically apply same function argument to different types:
f(id : (A) => A) =>
print(id(32))
print(id("abc")) // error, id is monomorphic
Using FCP we can write
data Id = (A) => A
f(id : Id) =>
print(id(32))
print(id("abc")) // no error, id is polymorphic
To write this with higher ranked types would require:
f(id : for<A> (A) => A) =>
print(id(32))
print(id("abc")) // no error, id is polymorphic
Note, you cannot use the location of the where clause to infer the scoping of the universal quantifier because there are no constraints on the identity function.
@keean wrote:
Using FCP we can write
data Id = Id((A) => A) f(id : Id) => print(id(32)) print(id("abc")) // no error, id is polymorphic
That is the same as the Rust example I have cited several times.
And that can solved without FCP employing unions:
f(id : (Int | String) => A) =>
print(id(32))
print(id("abc")) // no error, id has the right type
Or intersections:
f(id : ((Int) => A) + (String) => A) =>
print(id(32))
print(id("abc")) // no error, id has the right type
This is not a valid type:
(Int | String) => A
This works:
((Int) => A) + (String) => A)
But we haven't committed to intersection types, and the FCP example will work for all types not just the listed ones, so it is more general.
Very long types are not a good thing. Being able to write short types to avoid boilerplate is important. In this case the FCP type is more general and less boilerplate than the intersection type, especially if it is applied to more than two types inside f.
@keean wrote:
Using FCP we can write
data Id = Id((A) => A) f(id : Id) => print(id(32)) print(id("abc")) // no error, id is polymorphic
The function Id as written can't have any operations on A so it is useless. So A would need to be a typeclass object (in which case we don't need the FCP Id wrapper as it is redundant), else we would have to do monomorphization of the callback's typeclass bounds and I think it was explained upthread that in general that is not possible.
You can do:
data Sq = Sq((A) => A) requires Square<A> // this is polymorphic function argument
f(g : Sq) =>
print(g(32)) // we can monomorphise print as we know g returns an int
This is now a function that operates on any type that implements Square. However note the difference between this and:
data Sq = Sq(A) requires Square<A> // this is a typeclass-object
f(g : Sq -> Sq) =>
print(g(32)) // we have to defer dispatch of print to runtime as we do not know what type 'g' returns.
In the first case the function knows the return type is the same as the type passed to the square function, whereas in the second we do not know which type is returned from the function passed.
So you can see FCP generalises typeclass-objects to functions and other datatypes.
refresh once more
@keean wrote:
This is not a valid type:
(Int | String) => A
Yes it is. The function can test which type the input is.
This works:
((Int) => A) + (String) => A)But we haven't committed to intersection types
I believe we will eventually realize we can't have unions if we don't have intersections, especially if we want to adhere to principal types (not to be confused with principal typings as you did). We can't add half of a dual in the programming language, because first-class functions transpose the direction of variance (Top versus Bottom) for each nesting of argument (even if you think subtyping is possible to avoid and I believe you are incorrect once we add unions combined with first-class functions).
Edit: please note @keean and I revolved the misunderstanding linked above.
and the FCP example will work for all types not just the listed ones, so it is more general.
In this case the FCP type is more general
Not as it was originally written. It can (as changed) only apply to typeclass bounds which will early binding the operations of the callback and prevent the generality of extending the operations.
Very long types are not a good thing. Being able to write short types to avoid boilerplate is important.
Off-topic peevish point. Expression is priority # 1.
Expression is priority # 1.
FCP types are more expressive for some types, generally the ones you do not want limited to some fixed list of types.
Yes it is. The function can test which type the input is.
No it isn't because what is A... you cannot lift a type from runtime to compiletime without dependent typing. Perhaps I should have said, that would require dependent typing. It is not a valid type in the type system we have been discussing so far.
I believe we will eventually realize we can't have unions if we don't have intersections
They are not a requirement. You can easily have a type system restricted to rank 0 or 1 union types. Thats not to say we don't want intersection types. I too think we might want them, I just don't think we need them as FCP types with typeclass bounds are more generic.
Not as it was originally written. It can (as changed) only apply to typeclass bounds which will early binding the operations of the callback and prevent the generality of extending the operations.
I am not sure I understand your point. This type:
data Sq = Sq((A) => A) requires Square<A>
can be applied to any type that implements Square. If that type is a union then which particular implementation of square can be deferred to runtime, however we still know statically that whatever type that is, the result of the 'Sq' function will be the same type.
not to be confused with principal typings as you did
I don't think you have that right, I was pointing out to you what a principal type and principal typing was, so I don't expect that kind of low attack from you!
@keean wrote:
not to be confused with principal typings as you did
I don't think you have that right, I was pointing out to you what a principal type and principal typing was, so I don't expect that kind of low attack from you!
No I pointed it out to you 12 days before you did to me. And please click the quoted link to your mistake about Ceylon.
No I pointed it out to you 12 days before you did to me. And please click the quoted link to your mistake about Ceylon.
And do you really think I didn't know what a principal typing was before then. Just because I was polite and didn't pick you up on it at the time, does not mean that I will put up with this kind of incorrect statement indefinitely.
I can refer you to LtU posts from years ago dealing with principal typings if you really want to go down that road...
No I pointed it out to you 12 days before you did to me. And please click the quoted link to your mistake about Ceylon.
And do you really think I didn't know what a principal typing was before then.
No, but I wasn't the one implying that I didn't know when I had cited 12 days before that the canonical research paper from decades ago.
Edit: I think you are the one who caused me to look up the Jim Trevor paper back in May. So technically you taught me, but I am referring to recent events.
Just because I was polite and didn't pick you up on it at the time, does not mean that I will put up with this kind of incorrect statement indefinitely.
What incorrect statement? I pointed out that Gavin King is saying "principle typings" where he really means "principle types" and then you responded and ignored my question and wrote "principal typings".
What incorrect statement? I pointed out that Gavin King is saying "principle typings" where he really means "principle types" and then you responded and ignored my question and wrote "principle typings".
Which means what exactly?
What are you trying to say? You obviously have some great insight into what I was thinking when I wrote that, so I wondered if you could explain what was going on?
Did you forget that 12 days ago I cited Jim Trevor's research paper which explains the difference between principal types and typings?
Maybe I was thinking about principal typings? A type system must have principal types in order to have principal typings. My point was Cylon was dealing with principal types of unions and intersections and I want to have a type system with principal typings. When I said I needed to think about it, that was because it is not immediately clear how this would be affected by principal typings. If I was only thinking about principal types then I would not need to think because the Cylon article summarised it quite well. I entirely missed they were calling it the wrong thing because I only looked at the code and the type equations...
Still I am just as bad as you, because I explained to you what principal typings were when you already knew, and had just written something that was a bit unclear :-)
My main issue was you didn't clarify if I was correct that Gavin King is abusing the term "principal typings" as Jim Trevor's paper (and the Wikipedia link) points out. I was too tired to follow up on it until now and it didn't seem worth wrangling over at the time.
So you know that I know what principal typings are, so I am not quite sure what you are trying to get at? It is highly likely I read your post quickly, didn't really think about it a lot, looked at the Cylon article and then started thinking about what this would mean in the context of the kind of type system I think we should have.
So you know that I know what principal typings are, so I am not quite sure what you are trying to get at?
Checking whether you know the difference between principle types and typings (and its relevance to why we may need both unions and intersections). Just because I know you know the latter, doesn't mean I know you know the former, especially when you replied to my Ceylon point seeming to indicate that you didn't know the difference. Now you've explained that you were rushing and ignored my question.
You can do:
data Sq = Sq((A) => A) requires Square<A> // this is polymorphic function argument f(g : Sq) => print(g(32)) // we can monomorphise print as we know g returns an int
But you can't monomorphize g, although that is an optimization peeve, not an expression issue.
Expression is priority # 1.
FCP types are more expressive for some types, generally the ones you do not want limited to some fixed list of types.
But now the caller of f is limited to providing Square operations. So it is trade-off. You get generalization of the callback, but lose the solution to the Expression Problem.
That is a negative in terms of expression. Generality (is just a convenience) doesn't trump extensibility (which is essential to composition).
Edit: seems the only way to get both is rank-2 (higher-ranked) typing? But inference becomes undecidable.
I am not sure I understand your point.
Now you do?
But you can't monomorphize g, although that is an optimization peeve, not an expression issue.
Actually you can in that example, but maybe not generally.
But now the caller of f is limited to providing Square operations. So it is trade-off. You get generalization of the callback, but lose the solution to the Expression Problem.
The intersection type would allow any method to be called, but restricts the types to the arguments of one of the intersected function types.
seems the only way to get both is rank-2 (higher-ranked) typing?
I am not sure it helps. But FCP gives us everything rank-2 types do.
Yes it is. The function can test which type the input is.
No it isn't because what is
A... you cannot lift a type from runtime to compiletime without dependent typing. Perhaps I should have said, that would require dependent typing. It is not a valid type in the type system we have been discussing so far.
The input argument type is static. The function knows that it will only receive an Int | String. There is no dependent typing needed. It is a valid static compile-time type.
Edit: I wasn't talking about making the result type match the input types, which is clear from the function signature I wrote (Int | String) => A.
This might work.
f(g : (A = Int | String) => A) =>
So we label Int | String as A so we can make sure we return the same type.
Please don't make endless noise wrangling on this point. Think it over carefully first, if you decide to disagree again.
If you think about the following type you should see why it cannot work:
f(g : (Int | String) => (A, B))
In this type:
(Int | String) => A
A is bottom.
Ais bottom.
Yup. How many times do I have to say I wasn't concerned about what print does. I was focusing only on the concept of the union as the input type. I was entirely ignoring the result type. Bottom is not an invalid type.
You should not use a free type variable as a substitute for bottom... if you mean:
(Int | String) => Bottom
You should write it. In general you cannot just magic type variables out of thin air, type variables that occur in a function return type must appear in the argument type.
I think this is useful though:
data Fn = Fn((A) => A requires IntOrString<A>)
@keean wrote:
You should not use a free type variable as a substitute for bottom... if you mean:
(Int | String) => Bottom
Arguing about which notation we are going to use when we are trying to have a discussion about concepts using pseudocode seems peevish.
On 11 Oct 2016, at 03:02, shelby3 notifications@github.com wrote:
@shelby3 wrote:
What concerns me overall is how complex this is becoming. I’d prefer to find some simplification.
I agree. So listen. The way forward is to implement something basic.
Write code with it. Then discuss how to extend it.
This morning Oz time I woke up to 36 emails in just this one issue list.
I developed Felix over 20 years by making incremental improvements
to working code using regression tests to ensure stuff either kept working
or could be easily fixed so it would. Something I did not achieve however
was an audience to provide feedback. Users provide the direction and drive
the choice of what to do next. Hard stuff like languages needs use cases
to make choices.
—
john skaller
skaller@users.sourceforge.net
http://felix-lang.org
I agree. So listen. The way forward is to implement something basic.
Write code with it. Then discuss how to extend it.
Sure, that's what I am doing. Did you get commit notification for the latest checkin?
@keean wrote:
This might work.
f(g : (A = Int | String) => A) =>So we label
Int | StringasAso we can make sure we return the same type.
I was thinking:
f(g : (A: Int | String) => A) =>
As shorthand for:
f(g : (Int | String) => A) where A: Int | String =>
I agree. So listen. The way forward is to implement something basic.
Write code with it. Then discuss how to extend it.
Sure, that's what I am doing. Did you get commit notification for the latest checkin?
Disagree. I want to know where we are headed. And I want to understand what the design axes are.
But you are guys are free of course to go on without me if you wish. I am not trying to force anyone to hash out the design issues now if they don't want to.