fbpx
Wikipedia

Structural type system

A structural type system (or property-based type system) is a major class of type systems in which type compatibility and equivalence are determined by the type's actual structure or definition and not by other characteristics such as its name or place of declaration. Structural systems are used to determine if types are equivalent and whether a type is a subtype of another. It contrasts with nominative systems, where comparisons are based on the names of the types or explicit declarations, and duck typing, in which only the part of the structure accessed at runtime is checked for compatibility.

Description

In structural typing, an element is considered to be compatible with another if, for each feature within the second element's type, a corresponding and identical feature exists in the first element's type. Some languages may differ on the details, such as whether the features must match in name. This definition is not symmetric, and includes subtype compatibility. Two types are considered to be identical if each is compatible with the other.

For example, OCaml uses structural typing on methods for compatibility of object types. Go uses structural typing on methods to determine compatibility of a type with an interface. C++ template functions exhibit structural typing on type arguments. Haxe uses structural typing, but classes are not structurally subtyped.

In languages which support subtype polymorphism, a similar dichotomy can be formed based on how the subtype relationship is defined. One type is a subtype of another if and only if it contains all the features of the base type, or subtypes thereof. The subtype may contain added features, such as members not present in the base type, or stronger invariants.

A distinction exists between structural substitution for inferred and non-inferred polymorphism. Some languages, such as Haskell, do not substitute structurally in the case where an expected type is declared (i.e., not inferred), e.g., only substitute for functions that are signature-based polymorphic via type inference.[1] Then it is not possible to accidentally subtype a non-inferred type, although it may still be possible to provide an explicit conversion to a non-inferred type, which is invoked implicitly.

Structural subtyping is arguably more flexible than nominative subtyping, as it permits the creation of ad hoc types and protocols; in particular, it permits creation of a type which is a supertype of an existing type, without modifying the definition of the latter. However, this may not be desirable where the programmer wishes to create closed abstractions.

A pitfall of structural typing versus nominative typing is that two separately defined types intended for different purposes, but accidentally holding the same properties (e.g. both composed of a pair of integers), could be considered the same type by the type system, simply because they happen to have identical structure. One way this can be avoided is by creating one algebraic data type for each use.

In 1990, Cook, et al., proved that inheritance is not subtyping in structurally-typed OO languages.[2]

Checking that two types are compatible, based on structural typing, is a non-trivial operation, e.g., requires maintaining a stack of previous checked types.[3]

Example

Objects in OCaml are structurally typed by the names and types of their methods.

Objects can be created directly (immediate objects) without going through a nominative class. Classes only serve as functions for creating objects.

 # let x = object val mutable x = 5 method get_x = x method set_x y = x <- y end;;  val x : < get_x : int; set_x : int -> unit > = <obj> 

Here the OCaml interactive runtime prints out the inferred type of the object for convenience. Its type (< get_x : int; set_x : int -> unit >) is defined only by its methods. In other words, the type of x is defined by the method types "get_x : int" and "set_x : int -> unit" rather than by any name.[4]

To define another object, which has the same methods and types of methods:

 # let y = object method get_x = 2 method set_x y = Printf.printf "%d\n" y end;;  val y : < get_x : int; set_x : int -> unit > = <obj> 

OCaml considers them the same type. For example, the equality operator is typed to only take two values of the same type:

 # x = y;;  - : bool = false 

So they must be the same type, or else this wouldn't even type-check. This shows that equivalence of types is structural.

One can define a function that invokes a method:

 # let set_to_10 a = a#set_x 10;;  val set_to_10 : < set_x : int -> 'a; .. > -> 'a = <fun> 

The inferred type for the first argument (< set_x : int -> 'a; .. >) is interesting. The .. means that the first argument can be any object which has a "set_x" method, which takes an int as argument.

So it can be used on object x:

 # set_to_10 x;;  - : unit = () 

Another object can be made that happens to have that method and method type; the other methods are irrelevant:

 # let z = object method blahblah = 2.5 method set_x y = Printf.printf "%d\n" y end;;  val z : < blahblah : float; set_x : int -> unit > = <obj> 

The "set_to_10" function also works on it:

 # set_to_10 z;; 10 - : unit = () 

This shows that compatibility for things like method invocation is determined by structure.

Let us define a type synonym for objects with only a "get_x" method and no other methods:

 # type simpler_obj = < get_x : int >;;  type simpler_obj = < get_x : int > 

The object x is not of this type; but structurally, x is of a subtype of this type, since x contains a superset of its methods. So x can be coerced to this type:

 # (x :> simpler_obj);;  - : simpler_obj = <obj>  # (x :> simpler_obj)#get_x;;  - : int = 10 

But not object z, because it is not a structural subtype:

# (z :> simpler_obj);; This expression cannot be coerced to type simpler_obj = < get_x : int >; it has type < blahblah : float; set_x : int -> unit > but is here used with type < get_x : int; .. > The first object type has no method get_x 

This shows that compatibility for widening coercions are structural.

References

  1. ^ "Signature-based polymorphism".
  2. ^ Cook, W.R.; Hill, W.L.; Canning, P.S. (January 1990). "Inheritance is not subtyping". Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages. San Francisco, California: 125–135. doi:10.1145/96709.96721. ISBN 978-0897913430. S2CID 8225906.
  3. ^ "Type compatibility: name vs structural equivalence".
  4. ^ "Object types".

External links

structural, type, system, this, article, needs, additional, citations, verification, please, help, improve, this, article, adding, citations, reliable, sources, unsourced, material, challenged, removed, find, sources, news, newspapers, books, scholar, jstor, j. This article needs additional citations for verification Please help improve this article by adding citations to reliable sources Unsourced material may be challenged and removed Find sources Structural type system news newspapers books scholar JSTOR July 2011 Learn how and when to remove this template message A structural type system or property based type system is a major class of type systems in which type compatibility and equivalence are determined by the type s actual structure or definition and not by other characteristics such as its name or place of declaration Structural systems are used to determine if types are equivalent and whether a type is a subtype of another It contrasts with nominative systems where comparisons are based on the names of the types or explicit declarations and duck typing in which only the part of the structure accessed at runtime is checked for compatibility Contents 1 Description 2 Example 3 References 4 External linksDescription EditIn structural typing an element is considered to be compatible with another if for each feature within the second element s type a corresponding and identical feature exists in the first element s type Some languages may differ on the details such as whether the features must match in name This definition is not symmetric and includes subtype compatibility Two types are considered to be identical if each is compatible with the other For example OCaml uses structural typing on methods for compatibility of object types Go uses structural typing on methods to determine compatibility of a type with an interface C template functions exhibit structural typing on type arguments Haxe uses structural typing but classes are not structurally subtyped In languages which support subtype polymorphism a similar dichotomy can be formed based on how the subtype relationship is defined One type is a subtype of another if and only if it contains all the features of the base type or subtypes thereof The subtype may contain added features such as members not present in the base type or stronger invariants A distinction exists between structural substitution for inferred and non inferred polymorphism Some languages such as Haskell do not substitute structurally in the case where an expected type is declared i e not inferred e g only substitute for functions that are signature based polymorphic via type inference 1 Then it is not possible to accidentally subtype a non inferred type although it may still be possible to provide an explicit conversion to a non inferred type which is invoked implicitly Structural subtyping is arguably more flexible than nominative subtyping as it permits the creation of ad hoc types and protocols in particular it permits creation of a type which is a supertype of an existing type without modifying the definition of the latter However this may not be desirable where the programmer wishes to create closed abstractions A pitfall of structural typing versus nominative typing is that two separately defined types intended for different purposes but accidentally holding the same properties e g both composed of a pair of integers could be considered the same type by the type system simply because they happen to have identical structure One way this can be avoided is by creating one algebraic data type for each use In 1990 Cook et al proved that inheritance is not subtyping in structurally typed OO languages 2 Checking that two types are compatible based on structural typing is a non trivial operation e g requires maintaining a stack of previous checked types 3 Example EditObjects in OCaml are structurally typed by the names and types of their methods Objects can be created directly immediate objects without going through a nominative class Classes only serve as functions for creating objects let x object val mutable x 5 method get x x method set x y x lt y end val x lt get x int set x int gt unit gt lt obj gt Here the OCaml interactive runtime prints out the inferred type of the object for convenience Its type lt get x int set x int gt unit gt is defined only by its methods In other words the type of x is defined by the method types get x int and set x int gt unit rather than by any name 4 To define another object which has the same methods and types of methods let y object method get x 2 method set x y Printf printf d n y end val y lt get x int set x int gt unit gt lt obj gt OCaml considers them the same type For example the equality operator is typed to only take two values of the same type x y bool false So they must be the same type or else this wouldn t even type check This shows that equivalence of types is structural One can define a function that invokes a method let set to 10 a a set x 10 val set to 10 lt set x int gt a gt gt a lt fun gt The inferred type for the first argument lt set x int gt a gt is interesting The means that the first argument can be any object which has a set x method which takes an int as argument So it can be used on object x set to 10 x unit Another object can be made that happens to have that method and method type the other methods are irrelevant let z object method blahblah 2 5 method set x y Printf printf d n y end val z lt blahblah float set x int gt unit gt lt obj gt The set to 10 function also works on it set to 10 z 10 unit This shows that compatibility for things like method invocation is determined by structure Let us define a type synonym for objects with only a get x method and no other methods type simpler obj lt get x int gt type simpler obj lt get x int gt The object x is not of this type but structurally x is of a subtype of this type since x contains a superset of its methods So x can be coerced to this type x gt simpler obj simpler obj lt obj gt x gt simpler obj get x int 10 But not object z because it is not a structural subtype z gt simpler obj This expression cannot be coerced to type simpler obj lt get x int gt it has type lt blahblah float set x int gt unit gt but is here used with type lt get x int gt The first object type has no method get x This shows that compatibility for widening coercions are structural References Edit Signature based polymorphism Cook W R Hill W L Canning P S January 1990 Inheritance is not subtyping Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages San Francisco California 125 135 doi 10 1145 96709 96721 ISBN 978 0897913430 S2CID 8225906 Type compatibility name vs structural equivalence Object types Pierce Benjamin C 2002 19 3 Types and Programming Languages MIT Press ISBN 978 0 262 16209 8 External links EditNominativeAndStructuralTyping at WikiWikiWeb Retrieved from https en wikipedia org w index php title Structural type system amp oldid 1136088295, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.