Concept# Type constructor

Summary

In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old ones. Basic types are considered to be built using nullary type constructors. Some type constructors take another type as an argument, e.g., the constructors for product types, function types, power types and list types. New types can be defined by recursively composing type constructors.
For example, simply typed lambda calculus can be seen as a language with a single non-basic type constructor—the function type constructor. Product types can generally be considered "built-in" in typed lambda calculi via currying.
Abstractly, a type constructor is an n-ary type operator taking as argument zero or more types, and returning another type. Making use of currying, n-ary type operators can be (re)written as a sequence of applications of unary type operators. Therefore, we can view the type operators as a simply typed

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related courses (2)

Related publications (1)

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a program part or a language. Students will learn how to apply these concepts in their reasoning.

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into the new web standard for portable binaries called WebAssembly ( https://webassembly.org/ )

Loading

Related people

No results

Related units

No results

In this thesis we study calculus of variations for differential forms. In the first part we develop the framework of direct methods of calculus of variations in the context of minimization problems for functionals of one or several differential forms of the type, $\int_{\Omega} f(d\omega), \quad \int_{\Omega} f(d\omega_{1}, \ldots, d\omega_{m}) \quad \text{ and } \int_{\Omega} f(d\omega, \delta\omega).$ We introduce the appropriate convexity notions in each case, called \emph{ext. polyconvexity}, \emph{ext. quasiconvexity} and \emph{ext. one convexity} for functionals of the type $\int_{\Omega} f(d\omega),$ \emph{vectorial ext. polyconvexity}, \emph{vectorial ext. quasiconvexity} and \emph{vectorial ext. one convexity} for functionals of the type $\int_{\Omega} f(d\omega_{1}, \ldots, d\omega_{m})$ and \emph{ext-int. polyconvexity}, \emph{ext-int. quasiconvexity} and \emph{ext-int. one convexity} for functionals of the type $\int_{\Omega} f(d\omega, \delta\omega).$ We study their interrelationships and the connections of these convexity notions with the classical notion of polyconvexity, quasiconvexity and rank one convexity in classical vectorial calculus of variations. We also study weak lower semicontinuity and weak continuity of these functionals in appropriate spaces, address coercivity issues and obtain existence theorems for minimization problems for functionals of one differential forms.\smallskip In the second part we study different boundary value problems for linear, semilinear and quasilinear Maxwell type operator for differential forms. We study existence and derive interior regularity and $L^{2}$ boundary regularity estimates for the linear Maxwell operator $\delta (A(x)d\omega) = f$ with different boundary conditions and the related Hodge Laplacian type system $\delta (A(x)d\omega) + d\delta\omega = f,$ with appropriate boundary data. We also deduce, as a corollary, some existence and regularity results for div-curl type first order systems. We also deduce existence results for semilinear boundary value problems \begin{align*} \left\lbrace \begin{gathered} \delta ( A (x) ( d\omega ) ) + f( \omega ) = \lambda\omega \text{ in } \Omega, \ \nu \wedge \omega = 0 \text{ on } \partial\Omega. \end{gathered} \right. \end{align*} Lastly, we briefly discuss existence results for quasilinear Maxwell operator \begin{align*} \delta ( A ( x, d \omega ) ) = f , \end{align*} with different boundary data.

Related concepts (7)

In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general, type theory is the academic study of type systems. Some type theorie

The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds func

In computer science and computer programming, a data type (or simply type) is a collection or grouping of data values, usually specified by a set of possible values, a set of allowed operations on t

Related lectures (7)