In type theory, a type system is said to have the principal type property if, given a term and an environment, there exists a principal type for this term in this environment, i.e. a type such that all other types for this term in this environment are an of the principal type.
| Attributes | Values |
|---|
| rdfs:label
| - Principal type (en)
- 主体类型 (zh)
|
| rdfs:comment
| - 在类型理论, 类型系统有主体类型t，当且仅当对于任意的类型环境A和表达式e，A |- e :u，都可以从t推导到u。 例如λ演算λx.x，其主体类型t=α -> α，α为类型变量，类似Java或C#的泛型类型变量。若有A|-λx.x: int -> int，令α=int，则可以从主体类型t具体化为int -> int。 类型系统希望具有主体类型，因为它可以对表达式确定一种单一类型，该单一类型可演化为该表达式的所有可能类型。如果类型系统没有主体类型，则一个表达式可能有多个互不兼容的类型。类型推导倾向于推导主体类型。 ML具有主体类型属性，ML表达式可以通过合一求出主体类型，该主体类型被算法用到。然而，一些ML的扩展，如，会令主体类型丧失（undecidable）。其他一些扩展，如Haskell的，也令主体类型丧失（destroy）。要么开发人员使用类型注解，要么编译器猜测类型。 主体类型与主体定型不同。主体定型意思是，对于表达式e，类型环境A和类型t为主体定型对，当且仅当对于任意的类型环境B和类型u（A、B有相同的变量），都可从(A,t)推导到(B,u)。该推导过程一般使用变量具体化和子类替换。 一般来说，有主体定型一定有主体类型；反之则不成立，例子是ML的let多态。 (zh)
- In type theory, a type system is said to have the principal type property if, given a term and an environment, there exists a principal type for this term in this environment, i.e. a type such that all other types for this term in this environment are an of the principal type. (en)
|
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| has abstract
| - In type theory, a type system is said to have the principal type property if, given a term and an environment, there exists a principal type for this term in this environment, i.e. a type such that all other types for this term in this environment are an of the principal type. The principal type property is a desirable one for a type system, as it provides a way to type expressions in a given environment with a type which encompasses all of the expressions' possible types, instead of having several incomparable possible types. Type inference for systems with the principal type property will usually attempt to infer the principal type. For instance, the ML system has the principal type property and principal types for an expression can be computed by Robinson's unification algorithm, which is used by the Hindley–Milner type inference algorithm. However, many extensions to the type system of ML, such as polymorphic recursion, can make the inference of the principal type undecidable. Other extensions, such as Haskell's generalized algebraic data types, destroy the principal type property of the language, requiring the use of type annotations or the compiler to "guess" the intended type from among several options. The principal typing property requires that, given a term, there exist a typing (i.e. a pair with a context and a type) which is an instance of all possible typings of the term. The principal typing property can be confused with the principle type property but is distinct. The principle type property relies on the context as an input to determine the type, but the principle typing property outputs the context as a result. (en)
- 在类型理论, 类型系统有主体类型t，当且仅当对于任意的类型环境A和表达式e，A |- e :u，都可以从t推导到u。 例如λ演算λx.x，其主体类型t=α -> α，α为类型变量，类似Java或C#的泛型类型变量。若有A|-λx.x: int -> int，令α=int，则可以从主体类型t具体化为int -> int。 类型系统希望具有主体类型，因为它可以对表达式确定一种单一类型，该单一类型可演化为该表达式的所有可能类型。如果类型系统没有主体类型，则一个表达式可能有多个互不兼容的类型。类型推导倾向于推导主体类型。 ML具有主体类型属性，ML表达式可以通过合一求出主体类型，该主体类型被算法用到。然而，一些ML的扩展，如，会令主体类型丧失（undecidable）。其他一些扩展，如Haskell的，也令主体类型丧失（destroy）。要么开发人员使用类型注解，要么编译器猜测类型。 主体类型与主体定型不同。主体定型意思是，对于表达式e，类型环境A和类型t为主体定型对，当且仅当对于任意的类型环境B和类型u（A、B有相同的变量），都可从(A,t)推导到(B,u)。该推导过程一般使用变量具体化和子类替换。 一般来说，有主体定型一定有主体类型；反之则不成立，例子是ML的let多态。 (zh)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage redirect
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)