Questions tagged [polymorphisms]
The polymorphisms tag has no usage guidance.
31
questions
3
votes
0
answers
26
views
Polymorphism in SMT solvers
What are the theoretical limitations that avoid the adoption of type polymorphism à la System F in current SMT solvers?
I work in the context of program verification and I am surprised by the great ...
- 2,196
1
vote
1
answer
49
views
Can we somehow get functoriality from purely type-theoretic reasoning?
In this question, I asked about how to prove naturality from parametric polymorphism, using parametricity. The current answer to that question simply assumes that the functors in question satisfy the ...
- 3,464
7
votes
2
answers
207
views
Rigorous proof that parametric polymorphism implies naturality using parametricity?
This question asks for an informal explanation of why all polymorphic functions between functors are natural transformations (This is a claim made by Bartosz Milewski). One answer to that question ...
- 3,464
1
vote
1
answer
26
views
"Reshaping" vs Polymorphism In Data Wrangling
A lot of the work in data science -- machine learning in particular --involves "reshaping" arrays, tables, and other data structures. These data transformations are not really lossy ...
- 378
2
votes
1
answer
329
views
What's the difference between Row Polymorphism and Structural Typing?
The definitions I've stumbled across seem to indicate they express the same idea. That's that the relationship between record types is determined by their fields (or properties) rather than their ...
- 243
4
votes
1
answer
382
views
Why do we need a separate notation for П-types?
Main
I am confused about the motivation behind the need for a separate notation for П-types, that you can find in type systems from λ2 on. The answer usually goes like so - think about how one can ...
- 205
2
votes
3
answers
113
views
Uncurrying and Polymorphism
How do we uncurry functions when they are polymorphic? For example, is it possible to uncurry the following types? If so what is the uncurried type?
$\forall X. X \rightarrow int \rightarrow X$ ?
$...
- 31
4
votes
1
answer
190
views
Why are all polymorphic functions between functors natural transformations?
Bartosz Milewski's Category Theory for Programmers says the following:
A parametrically polymorphic function between two functors (including the edge case of the Const functor) is always a natural ...
- 276
2
votes
2
answers
77
views
Are type variables really only used in mathematical conversation about types?
Are type variables really only used in mathematical conversation about types? i.e. are type variables (meta-variables that only contain the type classification label) only exist in proofs for types ...
- 2,910
1
vote
1
answer
159
views
What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?
I was studying polymorphic types and I was finding the distinction with monomorphic types difficult to pin down (context CS 421). From the course I linked the have the following (vague attempt) at a ...
- 2,910
5
votes
1
answer
104
views
What does $ \forall \alpha_1, \dots , \alpha_n . \tau $ mean formally as a type?
I was learning about polymorphic types but I couldn't understand the notation, can someone explain it means (context cs421 UIUC):
$$ \forall \alpha_1, \dots , \alpha_n . \tau $$
its supposed to be a ...
- 2,910
1
vote
0
answers
96
views
Do Rank-1 (prenex) polymorphism and Predicative polymorphism mean the same?
https://en.wikipedia.org/wiki/Parametric_polymorphism says:
Rank-1 (prenex) polymorphism
In a prenex polymorphic system, type variables may not be instantiated with polymorphic types.[4] ...
- 1
1
vote
0
answers
77
views
What are the relation and differences between reification and type passing semantics?
https://en.wikipedia.org/wiki/Type_erasure says
type erasure refers to the load-time process by which explicit type annotations are removed from a program, before it is executed at run-time. ...
- 1
1
vote
2
answers
276
views
How can an existential type be defined in terms of universal type?
In Types and Programming Languages by Pierce, how does the following achieve the definition of an existential type in terms of universal type, by polymorphic version of Church encoding of pairs?
...
- 1
0
votes
1
answer
72
views
Why are ADT packages opened immediately after they are built, while existential objects opened as late as possible?
Section 24.2 in Types and Programming Languages by Pierce defines ADTs in existential types:
A conventional abstract data type (or ADT) consists of (1) a type name A, (2) a concrete representation ...
- 1
0
votes
1
answer
132
views
How can mainstream OO languages support strong binary operations by classes?
Section 24.2 in Types and Programming Languages by Pierce compares ADT and existential objects,in terms of how well they support strong binary operations:
Other binary operations cannot be ...
- 1
1
vote
1
answer
58
views
Are type abstraction values and universal types not for non functions, but only for functions?
In Types and Programming Languages by Pierce, Chapter 23 Universal Types has a summary of System F in the following figure, in particular, "type abstraction values" and their types "universal types".
...
- 1
0
votes
1
answer
50
views
How does this allow list operations to be applied to lists with elements of any type?
In Types and Programming Languages by Pierce, Chapter 11 is simple extensions of the simply typed lambda calculus with any simple base types. Section 11.12 introduces Lists.
How does the section ...
- 1
1
vote
1
answer
44
views
What does it mean that a let-binding can be treated polymorphically, only if its right-hand side is a syntactic value?
Types and Programming Languages by Pierce says:
22.7 Let polymorphism
A final point worth mentioning is that, in designing full-blown
programming languages with let-polymorphism, we need to ...
- 1
1
vote
1
answer
39
views
What is the purpose of erasing a type application to a term-application in parametric polymorphism?
From Types and Programming Languages by Pierce
23 Polymorphism
23.7 Erasure and Evaluation Order
in a full-blown programming language, which may include side-
effecting features such as ...
- 1
2
votes
0
answers
116
views
Is it possible to write a fully-decidable type system for the J language?
I'm experimenting with the J array language, a dynamically-typed array language with mutable assignment, subtyping, and function overloading (just like traditional APL).
It is unclear to me whether ...
- 205
5
votes
3
answers
253
views
How exactly do we define parametric polymorphism?
My naive distinction between parametric polymorphism and ad-hoc polymorphism, is that:
In parametric polymorphism, the type is given as a variable: (pseudocode)
Function f: <.Type T> T $\to$ T {...
- 3,464
5
votes
0
answers
99
views
Which languages, if any, implemented parametric polymorphism before ML?
In particular, was there any kind of implementation at the time Christopher Strachey wrote Fundamental Concepts in Programming Languages?
In that work, Strachey lists Ad Hoc and Parametric ...
- 224
6
votes
1
answer
201
views
Relationship between Higher Kinded Polymorphism, type inference, and Currying
On Hacker News there is an interesting exchange about the async\await RFC for Rust.
The author of the proposal withoutboats is responding to a comment about the ...
- 113
2
votes
1
answer
138
views
How to implement polymorphism in a turing complete environment?
I'm currently programming in an unnamed turing complete language which has support for pointers, primitive data types, structures, closures, and garbage collection, among other things.
I'm trying to ...
- 131
7
votes
4
answers
2k
views
Is subtype polymorphism a kind of ad hoc polymorphism?
"Ad-hoc polymorphism is obtained when a function works, or appears to work, on several different types (which may not exhibit a common structure) and may behave in unrelated ways for each type." – ...
- 173
5
votes
1
answer
180
views
What's the advantage of "value restriction" over its alternatives?
What is the motivation to pick "value restriction" over other candidates?
Examples of alternatives:
Enclosing pureness into the function type, for example:
...
- 151
7
votes
2
answers
739
views
Higher-ranked polymorphism without explicit application or subtyping?
So, I'm familiar with two main strategies of having higher-ranked polymorphism in a language:
System-F style polymorphism, where functions are explicitly typed, and instantiation happens explicitly ...
- 29.1k
0
votes
2
answers
302
views
Can String be a subtype of Character in a programming language?
Could a programming language be designed so that there is an inheritance relationship between string and character (both of ...
- 325
3
votes
1
answer
195
views
how type checking fails?
I was doing a type checking example in system f sub on paper to understand how it works.
according to Pierce's book Types and Programming Languages, numbers and their types are following in system f ...
- 1,042
1
vote
1
answer
62
views
Can a $k$-ary relation have polymorphisms of arity greater than $k$?
To quote Hubie Chen's A Rendezvous of Logic, Complexity, and Algebra (2009) on constraint satisfaction and complexity,
An operation $f : D^m \to D$ is a polymorphism of a relation $R \subseteq D^k$
...
- 145