dict.org

The DICT Development Group


Search for:
Search type:
Database:

Database copyright information
Server information


1 definition found
 for generic type variable
From The Free On-line Dictionary of Computing (30 December 2018) :

  generic type variable
  schematic type variable
  
      (Or "schematic type variable") In typed
     programming languages, a generic type variable is a type
     variable that may be instantiated to different types in
     different occurrences in a type expression.  Thus, in the
     expression
  
     	let id x = x in
     	(id True, id 1)
  
     id's type is (for all a: a -> a).  The universal quantifier
     "for all a:" means that a is a generic type variable.  For the
     two uses of id, a is instantiated to Bool and Int.  Compare
     this with
  
     	let id x = x in
     	let f g = (g True, g 1) in
     	f id
  
     This looks similar but f has no legal Hindley-Milner type.
     If we say
  
     	f :: (a -> b) -> (b, b)
  
     this would permit g's type to be any specific instance of (a
     -> b) rather than requiring it to be at least as general as (a
     -> b).  Furthermore, it constrains both instances of g to have
     the same result type whereas they can not.  The type variables
     a and b in the above are implicitly quantified at the top
     level:
  
     	f :: for all a: for all b: (a -> b) -> (b, b)
  
     so instantiating them (removing the quantifiers) can only be
     done once, at the top level.  To correctly describe the type
     of f requires that they be locally quantified:
  
     	f :: ((for all a: a) -> (for all b: b)) -> (c, d)
  
     which means that each time g is applied, a and b may be
     instantiated differently.  f's actual argument must have a
     type at least as general as ((for all a: a) -> (for all b:
     b)), and may not be some less general instance of this type.
     Type variables c and d are still implicitly quantified at the
     top level and, now that g's result type is a generic type
     variable, any types chosen for c and d are guaranteed to be
     instances of it.
  
     This type for f does not express the fact that b only needs to
     be at least as general as the types c and d.  For example, if
     c and d were both Bool then any function of type (for all a: a
     -> Bool) would be a suitable argument to f but it would not
     match the above type for f.
  
     (2017-12-13)
  

Contact=webmaster@dict.org Specification=RFC 2229