Re: Python from Wise Guy's Viewpoint
Espen Vestre wrote:[color=blue]
> Now you're conflating two readings of "want declarations" (i.e. "want
> them whenever they're convenient for optimizing" vs. "want them
> everywhere and always")[/color]
Type inference is about "as much static checking as possible with as
little annotations as absolutely necessary".
HM typing is extremely far on the "few declarations" side: a handful
even in large systems.
It sounds unbelievable, but it really works.
Oh, there's one catch: Most functional programs have heaps of type
definitions similar to this one:
Tree a = Leaf a
| Node (Tree a) (Tree a)
| Empty
However, these definitions don't only declare the type, they also
introduce constructors, which also serve as inspectors for pattern matching.
In other words, the above code is all that's needed to allow me to
construct arbitrary values of the new type (gratuitious angle brackets
inserts to make the code easier to recognize with a C++ background),
like this:
Leaf 5 -- Creates a Leaf <Integer> object that contains value 5
Node Empty Empty -- Creates a node that doesn't have leaves
-- Type is Tree <anything>, i.e. we can insert this object into
-- a tree of any type, since there's no way that this can ever
-- lead to type errors.
Node (Leaf 5) (Leaf 6) -- Creates a node with two leaves
It also allows me to use the constructor names as tags for pattern
matching. Note that every one of the following three definitions
consists of the name of the function being defined, a pattern that the
arguments must follow to select this particular definition, and the
actual function body (which is just an expression here). Calling a
function with parameters that match neither pattern is considered an
error (which is usually caught at compile time but not in all cases -
not everything is static even in functional languages).
mapTree f (Leaf foo) = Leaf f foo
-- If mapTree if given a "something" called f,
-- and some piece of data that was constructed using Leaf foo,
-- then the result will be obtained by applying f as a function
-- to that foo, and making the result a Leaf.
-- The occurence of f in a function position on the right side
-- makes type inference recognize it as a function.
-- The Leaf pattern (and, incidentally, the use of the Leaf
-- constructor on the right side) will make type inference
-- recognize that the second parameter of mapTree must be
-- of Tree <anything> type. Usage details will also make
-- type inference conclude that f must be a function from
-- one "anything" type to another, potentially different
-- "anything" type.
-- In other words, the type of mapTree is known to be
-- (a -> b) -> Tree a -> Tree b
-- without a single type declaration in mapTree's code!
mapTree f (Node left right) = Node (maptree f left) (maptree f right)
-- This code is structured in exact analogy to the Leaf case.
-- The only difference is that it uses recursion to descend
-- into the subtrees.
-- Incidentally, this definition of mapTree
mapTree f Empty = Empty
-- The null value doesn't need to be mapped, it will look the
-- same on output.
-- Note that this definition of mapTree doesn't restrict the
-- type of f in the least.
-- In HM typing, you usually don't specify the types, every
-- usage of some object adds further restrictions what that
-- type can be. If the set of types that a name can have becomes
-- empty, you have contradictory type usage and hence a type error.
Hope this helps
Jo
Espen Vestre wrote:[color=blue]
> Now you're conflating two readings of "want declarations" (i.e. "want
> them whenever they're convenient for optimizing" vs. "want them
> everywhere and always")[/color]
Type inference is about "as much static checking as possible with as
little annotations as absolutely necessary".
HM typing is extremely far on the "few declarations" side: a handful
even in large systems.
It sounds unbelievable, but it really works.
Oh, there's one catch: Most functional programs have heaps of type
definitions similar to this one:
Tree a = Leaf a
| Node (Tree a) (Tree a)
| Empty
However, these definitions don't only declare the type, they also
introduce constructors, which also serve as inspectors for pattern matching.
In other words, the above code is all that's needed to allow me to
construct arbitrary values of the new type (gratuitious angle brackets
inserts to make the code easier to recognize with a C++ background),
like this:
Leaf 5 -- Creates a Leaf <Integer> object that contains value 5
Node Empty Empty -- Creates a node that doesn't have leaves
-- Type is Tree <anything>, i.e. we can insert this object into
-- a tree of any type, since there's no way that this can ever
-- lead to type errors.
Node (Leaf 5) (Leaf 6) -- Creates a node with two leaves
It also allows me to use the constructor names as tags for pattern
matching. Note that every one of the following three definitions
consists of the name of the function being defined, a pattern that the
arguments must follow to select this particular definition, and the
actual function body (which is just an expression here). Calling a
function with parameters that match neither pattern is considered an
error (which is usually caught at compile time but not in all cases -
not everything is static even in functional languages).
mapTree f (Leaf foo) = Leaf f foo
-- If mapTree if given a "something" called f,
-- and some piece of data that was constructed using Leaf foo,
-- then the result will be obtained by applying f as a function
-- to that foo, and making the result a Leaf.
-- The occurence of f in a function position on the right side
-- makes type inference recognize it as a function.
-- The Leaf pattern (and, incidentally, the use of the Leaf
-- constructor on the right side) will make type inference
-- recognize that the second parameter of mapTree must be
-- of Tree <anything> type. Usage details will also make
-- type inference conclude that f must be a function from
-- one "anything" type to another, potentially different
-- "anything" type.
-- In other words, the type of mapTree is known to be
-- (a -> b) -> Tree a -> Tree b
-- without a single type declaration in mapTree's code!
mapTree f (Node left right) = Node (maptree f left) (maptree f right)
-- This code is structured in exact analogy to the Leaf case.
-- The only difference is that it uses recursion to descend
-- into the subtrees.
-- Incidentally, this definition of mapTree
mapTree f Empty = Empty
-- The null value doesn't need to be mapped, it will look the
-- same on output.
-- Note that this definition of mapTree doesn't restrict the
-- type of f in the least.
-- In HM typing, you usually don't specify the types, every
-- usage of some object adds further restrictions what that
-- type can be. If the set of types that a name can have becomes
-- empty, you have contradictory type usage and hence a type error.
Hope this helps
Jo
Comment