New answers tagged type-theory
0
Thanks to the commenters above. They suggest a grammar definition for parsing. Here's one in PyPEG2 (untested and incomplete), but shows how I'll handle variable and sub/superscripting.
from term import Term
from pypeg2 import *
alphabet = RegEx( r'\alpha|\beta|\gamma|\delta|\epsilon|' + \
r'\zeta|\eta|\theta|\vartheta|\iota|' + \
...
2
Here is a new paper that covers a similar topic. The idea is that by doing algebra in enriched categories (2-categories are like categories enriched in categories), you can talk about more fine grained semantic structure on the algebra. (I haven't read through the whole paper myself, but I know enough to see some of the ideas behind it.)
The way it relates ...
1
Yes, in that context Hindley-Milner polymorphism is let-polymorphism, since such language uses $\sf let$ to introduce polymorphic functions.
In the untyped lambda calculus, we can consider a (non recursive)
${\sf let}\ x = e \ {\sf in}\ t$ to be syntactic sugar for
$(\lambda x.t)e$.
In System F, where polymorphism is introduced by explicit $\Lambda \alpha$ ...
1
There is just nothing that you can generalise. Every language is different.
A class describes what instances of the class (objects) look like. In Java, a class is also an object in its own right. All classes are instances of a class named "class", which allows the programmer to ask the class for example "what is your name", "what are the instance variables ...
2
I'm not confident enough about the later questions, but I hope I can give a partial answer, since this hasn't been given much love.
Yes
Yes
There is nothing in particular, since first-order logic quantifies over non-logical objects, but a priori there are no non-logical objects we're reasoning about for the lambda calculus. There is a similar-sounding type ...
3
Unfortunately I don't have a copy of TAPL with me, so I can't figure out exactly what the author intends. But there is a point we should make, that types are something which classifies terms or values, even if there are other pieces that are related to the type.
As such, classes and interfaces are not literally types themselves in Java or C++. Rather, each ...
0
In the Gaster and Jones paper, rows are encoded using type application of a few type constants, most notably row extension. Your implementation needs to have the following constructors in Typeconstant:
data Typeconstant = Arrow | EmptyRow | Rec | Var | RowExtension Label
Absence of labels is handled using predicates in qualified types:
data QualifiedType =...
Top 50 recent answers are included
