dict.org

The DICT Development Group


Search for:
Search type:
Database:

Database copyright information
Server information


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

  type inference
  
      An algorithm for ascribing types to
     expressions in some language, based on the types of the
     constants of the language and a set of type inference rules
     such as
  
     	f :: A -> B,  x :: A
     	---------------------  (App)
     	      f x :: B
  
     This rule, called "App" for application, says that if
     expression f has type A -> B and expression x has type A then
     we can deduce that expression (f x) has type B.  The
     expressions above the line are the premises and below, the
     conclusion.  An alternative notation often used is:
  
     	G |- x : A
  
     where "|-" is the turnstile symbol ({LaTeX \vdash) and G is a
     type assignment for the free variables of expression x.  The
     above can be read "under assumptions G, expression x has type
     A".  (As in Haskell, we use a double "::" for type
     declarations and a single ":" for the infix list constructor,
     cons).
  
     Given an expression
  
     	plus (head l) 1
  
     we can label each subexpression with a type, using type
     variables X, Y, etc. for unknown types:
  
     	(plus :: Int -> Int -> Int)
     		(((head :: [a] -> a) (l :: Y)) :: X)
     		(1 :: Int)
  
     We then use unification on type variables to match the
     partial application of plus to its first argument against
     the App rule, yielding a type (Int -> Int) and a substitution
     X = Int.  Re-using App for the application to the second
     argument gives an overall type Int and no further
     substitutions.  Similarly, matching App against the
     application (head l) we get Y = [X].  We already know X = Int
     so therefore Y = [Int].
  
     This process is used both to infer types for expressions and
     to check that any types given by the user are consistent.
  
     See also generic type variable, principal type.
  
     (1995-02-03)
  

Contact=webmaster@dict.org Specification=RFC 2229