type inference

23 results back to index


pages: 226 words: 17,533

Programming Scala: tackle multicore complexity on the JVM by Venkat Subramaniam

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

augmented reality, continuous integration, domain-specific language, loose coupling, semantic web, type inference, web application

If you attempt to assign some other type of value or instance to any of these variables, you’ll get a compilation error. Scala’s type inference is low ceremony1 and has no learning curve; you simply have to undo some Java practices. Scala’s static typing helps you in two ways. First, the compile-time type checking can give you confidence that the compiled code meets certain 1. See “Essence vs. Ceremony” in Appendix A, on page 211. Download at Boykma.Com Prepared exclusively for sam kaplan C OLLECTIONS AND T YPE I NFERENCE expectations.2 Second, it helps you to express the expectations on your API in a compiler-verifiable format. In this chapter, you’ll learn about Scala’s sensible static typing and type inference. You’ll also look at three special types in Scala: Any, Nothing, and Option. 5.1 Collections and Type Inference Scala will provide type inference and type safety for the Java Generics collections as well.

In other words, while AnyRef directly maps to Object, Any and AnyVal are type erased to Object much like type erasure of Generics parameterized types in Java. 5.3 More About Nothing You can see why you’d need Any, but what is the purpose of Nothing? Scala’s type inference works hard to determine the type of expressions and functions. If the type inferred is too broad, it will not help type verification. At the same time, how do you infer the type of an expression or function if one branch returns, say, an Int and another branch throws an exception? In this case, it is more useful to infer the type as Int rather than a general Any. This means that the branch that throws Download at Boykma.Com Report erratum Prepared exclusively for sam kaplan this copy is (P1.0 printing, June 2009) 67 O PTION T YPE the exception must be inferred to return an Int or a subtype of Int for it to be compatible. However, an exception may occur at any place, so not all those expressions can be inferred as Int. Scala helps type inference work smoothly with the type Nothing, which is a subtype of all types.

. 1.6 Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 11 14 19 22 24 24 Getting Started 2.1 Downloading Scala . . . . . . . 2.2 Installing Scala . . . . . . . . . 2.3 Take Scala for a Ride . . . . . . 2.4 Scala on the Command Line . . 2.5 Running Scala Code as a Script 2.6 Scala from an IDE . . . . . . . . 2.7 Compiling Scala . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 26 27 28 30 31 32 32 Getting Up to Speed in Scala 3.1 Scala as Concise Java . . . . . . . 3.2 Scala Classes for Java Primitives . 3.3 Tuples and Multiple Assignments . 3.4 Strings and Multiline Raw Strings 3.5 Sensible Defaults . . . . . . . . . . 3.6 Operator Overloading . . . . . . . . 3.7 Scala Surprises for the Java Eyes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 34 37 38 40 41 43 45 Classes in Scala 4.1 Creating Classes . . . . . . . . . . . . . . . . . 4.2 Defining Fields, Methods, and Constructors 4.3 Extending a Class . . . . . . . . . . . . . . . . 4.4 Singleton Object . . . . . . . . . . . . . . . . . 4.5 Stand-Alone and Companion Objects . . . . 4.6 static in Scala . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 53 54 57 58 60 61 Prepared exclusively for sam kaplan . . . . . . . . . . . . . . . . . . Download at Boykma.Com CONTENTS 5 6 7 8 9 Sensible Typing 5.1 Collections and Type Inference . . . . 5.2 The Any Type . . . . . . . . . . . . . . 5.3 More About Nothing . . . . . . . . . . . 5.4 Option Type . . . . . . . . . . . . . . . 5.5 Method Return Type Inference . . . . 5.6 Passing Variable Arguments (Varargs) 5.7 Variance of Parameterized Type . . . . . . . . . . . . . . . . . . 63 64 66 67 68 69 70 71 . . . . . . . . . 75 75 76 78 80 81 83 84 87 88 . . . . . 91 91 94 95 97 99 . . . . . . . . . . 103 103 104 106 108 113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

 

pages: 554 words: 108,035

Scala in Depth by Tom Kleenex, Joshua Suereth

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

discrete time, domain-specific language, fault tolerance, MVC pattern, sorting algorithm, type inference

In C++, this is maximized in the usage of a pointer, because a pointer can be constant. Scala defines three variable types on the left-hand side, like var, val, and lazy val. These leave the type of the variable clean. In all instances, the type of the name x is Int. In addition to separating the concerns of how a variable behaves from the variable type, the placement of types on the right allows type inference to determine the type of the variables. 1.2.2. Type inference Scala performs type inference wherever possible. Type inference is when the compiler determines what the type annotation should be, rather than forcing the user to specify one. The user can always provide a type annotation, but has the option to let the compiler do the work. val x: Int = 5 val y = 5 This feature can drastically reduce the clutter found in some other typed languages. Scala takes this even further to do some level of inference on arguments passed into methods, specifically with first-class functions.

Although most consider the SeqLike classes to be an implementation detail, they’re important when implementing any sort of generic method against collections. SeqLike captures the original fully typed collection in its second type parameter. This allows the type system to carry the most specific type through a generic method so that it can be used in the return value. Deferring Type Inference of Parent-Class Type Parameters The need to defer the type inference for a type parameter Foo <: Seq[T] is necessary for supporting the Scala 2.8.x series. As of the Scala 2.9.x, the type inference algorithm was improved such that the implicit <:< parameter is no longer necessary. The next type parameter in the sort method is the cbf : CanBuildFrom[Coll, T, Coll]. The CanBuildFrom trait, when looked up implicitly, determines how to build new collections of a given type. The first type parameter represents the original collection type.

Why do we need reified type constraints? Sometimes it can help the type inferencer automatically determine types for a method call. One of the neat aspects of the type inferencing algorithm is that implicits can defer the resolution of types until later in the algorithm. Scala’s type inferencer works in a left-to-right fashion across parameter lists. This allows the types inferred from one parameter list to affect the types inferred in the next parameter list. A great example of this left-to-right inference is with anonymous functions using collections. Let’s take a look: scala> def foo[A](col: List[A])(f: A => Boolean) = null foo: [A](col: List[A])(f: (A) => Boolean)Null scala> foo(List("String"))(_.isEmpty) res1: Null = null The foo method defines two parameter lists with one type parameter: one that takes a list of the unknown parameter and another that takes a function using the unknown parameter.

 

pages: 647 words: 43,757

Types and Programming Languages by Benjamin C. Pierce

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

Albert Einstein, combinatorial explosion, experimental subject, finite state, Henri Poincaré, recommendation engine, sorting algorithm, Turing complete, Turing machine, type inference, Y Combinator

This family of approaches to type reconstruction has the advantage of relative simplicity and clean integration with the polymorphism of ML. A pragmatic approach to partial type reconstruction for systems involving both subtyping and impredicative polymorphism, called local type inference (or local type reconstruction), was proposed by Pierce and Turner (1998; also see Pierce and Turner, 1997; Hosoya and Pierce, 1999). Local type inference has appeared in several recent language designs, including GJ (Bracha, Odersky, Stoutamire, and Wadler, 1998) and Funnel (Odersky and Zenger, 2001), the latter introducing a more powerful form called colored local type inference (Odersky, Zenger, and Zenger, 2001). A simpler but less predictable greedy type inference algorithm was proposed by Cardelli (1993); similar algorithms have also been used in proofcheckers for dependent type theories, such as NuPrl (Howe, 1988) and Lego (Pollack, 1990).

Finding the source of type errors. 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 38–43, 1986. Wand, Mitchell. Complete type inference for simple objects. In Proceedings of the IEEE Symposium on Logic in Computer Science, Ithaca, NY, June 1987. 602 References Wand, Mitchell. Corrigendum: Complete type inference for simple objects. In Proceedings of the IEEE Symposium on Logic in Computer Science, 1988. Wand, Mitchell. Type inference for objects with instance variables and inheritance. Technical Report NU-CCS-89-2, College of Computer Science, Northeastern University, February 1989a. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994). Wand, Mitchell. Type inference for record concatenation and multiple inheritance. In Fourth Annual IEEE Symposium on Logic in Computer Science, pages 92–97, Pacific Grove, CA, June 1989b.

., 461 609 factorial, 52 fail, 16 failure vs. undefinedness, 16 families (of terms, types), 462 Featherweight Java, 247–264 fields, see instance variables; records finalizers, 515 finding type errors, 545 finite tree type, 285 finite-state generating function, 294 first-class polymorphism, 340 fixed point, 142–145 combinator, 65 of a generating function, 282 theorem (Tarski-Knaster), 283 typing, using recursive types, 273 FJ, see Featherweight Java flattened data structures, 341 Float type, 117 fold function, 63 fomsub implementation, 467–473 formal methods, lightweight, 1 Forsythe, 11, 199 Fortran, 8, 11 fragments of System F, 358–359 fragments of System Fω , 461 free variable, 55, 69 fresh variable, 120 full abstraction, 143 full beta-reduction, 56 full F<: , 391 fullequirec implementation, 267–280 fullerror implementation, 171–178 fullfomsub implementation, 389–409, 467–473 fullfsub implementation, 389–409, 417– 436 fullfsubref implementation, 411–416 fullisorec implementation, 275–278 fullomega implementation, 439–466 fullpoly implementation, 339–379 fullrecon implementation, 317–338 fullref implementation, 153–170, 225– 245 610 Index fullsimple implementation, 99–111, 117–146 fullsub implementation, 181–208 fulluntyped implementation, 51–73 fullupdate implementation, 475–489 <fun>, 118 function types, 99–100 functional languages, mostly, 153 functions, 16 higher-order, 58 multi-argument, 58 on types, see type operators Funnel, 409 FX, 11 garbage collection, 45, 158–165, 514– 515 tag free, 341 general recursion, 142–145 generating function, 282 generating set, 290 generation lemma, see inversion lemma generators, classes as, 229 generics, 341 gfp algorithm, 292, 295–298 GJ, 195, 248, 409 grammar, 24 graph reduction, 57 greatest fixed point of a generating function, 283 greatest lower bound, see joins and meets greedy type inference, 355 hash consing, 222 Haskell, 6, 45 heap, 153 hidden representation type, 364 higher-order bounded quantifiers, 468 higher-order functions, 58 higher-order polymorphism, 449–466 history of type systems, 10 hungry functions, 270 hybrid object models, 377 identity, object, 245 identity function, 55 imperative objects, see objects, imperative implementations allsome, 381–387 arith, 23–49 bot, 220 equirec, 281–313 fomsub, 467–473 fullequirec, 267–280 fullerror, 171–178 fullfomsub, 389–409, 467–473 fullfsub, 389–409, 417–436 fullfsubref, 411–416 fullisorec, 275–278 fullomega, 439–466 fullpoly, 339–379 fullrecon, 317–338 fullref, 153–170, 225–245 fullsimple, 99–111, 117–146 fullsub, 181–208 fulluntyped, 51–73 fullupdate, 475–489 joinexercise, 223 joinsub, 218–220 purefsub, 417–436 rcdsub, 181–224 recon, 317–338 reconbase, 330 simplebool, 113–116 tyarith, 91–98 untyped, 83–88 implicit type annotations, 330–331 implicitly typed languages, 101 impredicative polymorphism, 340, 360– 361 impure language features, 153 induction, 19 lexicographic, 19 logical relations proof technique, 150 mathematical foundations, 282–284 on derivations, 37 on natural numbers, 19 on terms, 29–32 Index inductive definitions, 23–29 inference, see type reconstruction inference rules, 26 mathematical foundations, 283 infinite types, 284–286 inheritance, 227 overrated, 245 injection into a sum type, 133 instance of an inference rule, 36 instance variables, 228, 230, 233–234 instanceof, 341 instantiation of a polymorphic function, 317–320, 342 intensional polymorphism, 340 interface, 226 interface types, 479 interfaces (in Java), 261 interference, syntactic control of, 170 intermediate language, 161 intermediate languages, typed, 11 internal language, 53, 120 internet, see web intersection types, 11, 206–207, 359, 489 and bounded quantification, 400, 409 and normal forms, 206 introduction rule, 108 invariant, 33 inversion lemma subtyping, 188 typing, 94, 104, 188, 457 iso-recursive types, 275, 280 subtyping, 311–312 Java, 6, 8–10, 45, 119, 137, 154, 174, 177, 178, 193, 195, 196, 198–199, 226, 232, 247–264, 341, 444 exception handling in, 174 parametric polymorphism, 195 reflection, 196 JINI, 9 joinexercise implementation, 223 joins and meets, 17 algorithms for calculating, 218–220 in System F<: , 432–435 611 joinsub implementation, 218–220 judgment, 36 KEA, 226 kernel F<: , 391 kinding, 439–447, 459 kinds dependent, 445 power, 445 row, 445 singleton, 445 Knaster-Tarski fixed point theorem, 283 λ-calculus, see lambda-calculus λNB, 63–66 λ→ , see simply typed lambda-calculus λω , see System λω λ<: , see simply typed lambda-calculus with subtyping label, 129 lambda cube, 465 lambda-& calculus, 226, 340 lambda-calculi, typed, 2 lambda-calculus, 51, 52 enriched, 63–68 simply typed, see simply typed lambdacalculus untyped, see untyped lambda-calculus lambda-term, 53 language definition, defined, 7 language design and type systems, 9– 10 language features, pure, 153 late binding, see objects, open recursion latent type system, 2 lazy evaluation, 57 least fixed point of a generating function, 283 least upper bound, see joins and meets left-associativity of application, 54 let bindings, 124–125 let-polymorphism, 331–336, 340 exponential behavior, 334 levels, de Bruijn, 81 612 Index lexical analysis, 53 lexicographic induction, 19 lexicographic order, 19 LF, 11, 465 lfp algorithm, 294 lightweight formal methods, 1 linear logic and type systems, 11, 109 linking, 367 lists, 146 Church encoding, 350–353, 500 defined using recursive types, 267– 270 polymorphic functions for, 345–347 subtyping, 197 local type inference, 355 location, 159 logic and type systems, 108 origins, 11 type systems in, 2 logical framework, 465 logical relations, 149 µ, see least fixed point µ notation for recursive types, 299– 304 marshaling, 252, 341 Martin-Löf type theory, see constructive type theory match function, 131 matching, pattern-, 130–131 matching relation on object types, 480 mathematics, formalization of, 11 meaning of terms, 32–34 meet, see joins and meets membership checking for (co-)inductively defined sets, 290–298 Mercury, 338 message, 226 meta-mathematics, 24 metalanguage, 24 metatheory, 24 metavariables, 24 naming conventions, 565 method, 226, 228 invocation, 226 multi-, see multi-method override, 233, 264 Milner-Mycroft Calculus, 338 minimal types, 218, 418–420 minimal typing theorem, 419 mini-ML, 337 ML, 6, 8, 9, 11, 174, 177 exception handling in, 174 history, 336–338 module system, 379 parametric datatypes, 445 polymorphism, 331–336 ML implementations evaluation, 87 simply typed lambda-calculus, 113– 116 subtyping, 221–224 System F, 381–387 untyped arithmetic expressions, 45– 49 untyped lambda-calculus, 83–88 ML-style polymorphism, 340 modal logics, 109 model checking, 1, 284 Modula-3, 7 modularity, 3 module systems, 364, 379, 465 monads, 153 monitoring, run-time, 1 monotone function, 282 monotype, 359 most general unifier, 327 mostly functional languages, 153 multi-argument functions, 58 multi-method, 226, 340 multiple inheritance, 489 multiple representations (of object types), 226 multi-step evaluation, 39 mutually recursive functions, 144 types, 253 Index ν, see greatest fixed point nameless form, see de Bruijn indices naming context, 77 naming conventions for metavariables and rules, 565–566 narrowing lemmas, 401, 425 National Science Foundation, xx natural deduction, 26 natural semantics, 32, 34, 43 natural-number induction, 19 nested induction, 19 NextGen, 196 nominal type systems, 251–254, 312 normal forms, 38 and intersection types, 206 uniqueness of, 39 normal order, 56 normalization, 149–152 by evaluation, 152 strong, 152 normalization theorem, 39, 152, 353 numeric values, 40 NuPRL, 11 object calculus, 11, 51, 184, 248, 251 object language, 24 Objective Caml see OCaml, xvii objects, 228, 368 as recursive records, 272 bounded quantification and, 411–416 encodings vs. primitive objects, 262– 263 existential, 372–377, 475–489 hybrid object models, 377 identity, 245 imperative, 157, 225–245, 411–416 interface types, 479 Java-style, 247–264 matching relation on object types, 480 object-oriented programming, defined, 225–227 open recursion, 227, 235–244 purely functional, 372–377, 475–489 613 vs. abstract data types, 374–377 OCaml, xvii, 7, 45, 208, 231, 489 OCaml implementations, see ML implementations occur check, 327, 338 omega, 65 open recursion, see objects, open recursion operational semantics, 32, see also evaluation big-step, 43 small-step, 42 operator associativity, 53 operator precedence, 53 Option type, 137–138 order, well-founded, 18 ordered sets, basic definitions, 16–18 ordinary induction, 19 overloading, 340 finitary, 206 overriding of method definitions, 233 P(S) powerset of S, 15 package, existential, 364 pairs, 126–127 Church encodings, see Church encodings, pairs parallel reduction, 454 parametric abbreviation, 439 data type, 142, 444 polymorphism, 319, 340 parametricity, 359–360 parentheses and abstract syntax, 25, 52 parsing, 53 partial evaluation, 109 partial function, 16 partial order, 17 partially abstract types, 406 Pascal, 11 pattern matching, 130–131 PCF, 143 Pebble, 465 Penn translation, 204 614 Index Perl, 6 permutation, 18 permutation lemma, 106 permutation rule for record subtyping, 184 performance issues, 201–202 pi-calculus, 51 Pict, 200, 356, 409 Pizza, 195 pointer, 154, see references arithmetic, 159 pointwise subtyping of type operators, 468 polarity, 473 PolyJ, 195 polymorphic functions for lists, 345–347 identity function, 342 recursion, 338 update, 482–485 polymorphism, 331 ad hoc, 340 data abstraction, 368–377 existential, see existential types existential types, 363–379 exponential behavior of ML-style, 334 F-bounded, 393, 408 higher-order, 449–466 impredicativity and predicativity, 360– 361 intensional, 340 ML-style, 331–336 parametric, 339–361 parametricity, 359–360 predicative, 360 prenex, 359 rank-2, 359 safety problems with references, 335– 336 stratified, 360 subtype, see subtyping universal, see universal types varieties of, 340–341 polytype, 359 portability, types and, 7 positive subtyping, 489 Postscript, 6 power types, 445, 472 precedence of operators, 53 predecessor for Church numerals, 62 predicate, 15 predicative polymorphism, 360–361 prenex polymorphism, 359 preorder, 17 preservation of a predicate by a relation, 16 preservation of shapes under type reduction, 456 preservation of types during evaluation, 95–98, 107, 168, 173, 189, 261, 353, 404, 457 preservation of typing under type substitution, 318 principal type, 317, 329–330 types theorem, 329 typing, 337 unifier, 327 principal solution, 329 principle of safe substitution, 182 product type, 126–127 programming languages Abel, 409 Algol-60, 11 Algol-68, 11 Amber, 311 C, 6, 45 C] , 7 C++, 6, 226 Cecil, 226, 340 Clean, 338 CLOS, 226, 340 CLU, 11, 408 Dylan, 226 Featherweight Java, 247–264 Forsythe, 11, 199 Fortran, 8, 11 Funnel, 409 615 Index FX, 11 GJ, 195, 248, 409 Haskell, 6, 45 Java, 6, 8–10, 45, 119, 137, 154, 174, 177, 178, 193, 195, 196, 198–199, 226, 232, 247–264, 341, 444 KEA, 226 Mercury, 338 ML, 6, 8, 9, 11, 174, 177, see also OCaml, Standard ML Modula-3, 7 NextGen, 196 Objective Caml, see OCaml OCaml, xvii, 7, 208, 231, 489 Pascal, 11 Pebble, 465 Perl, 6 Pict, 200, 356, 409 Pizza, 195 PolyJ, 195 Postscript, 6 Quest, 11, 409 Scheme, 2, 6, 8, 45 Simula, 11, 207 Smalltalk, 226 Standard ML, xvii, 7, 45 Titanium, 8 XML, 9, 207, 313 progress theorem, 38, 95–98, 105, 169, 173, 190, 262, 353, 405, 458 projection (from pairs, tuples, records), 126–131 promotion, 418 proof, defined, 20 proof-carrying code, 9 proof theory, 2 proper types, 442 propositions as types, 109 pure λ→ , 102 pure lambda-calculus, 51 pure language features, 153 pure type systems, xiv, 2, 444, 466 purefsub implementation, 417–436 qualified types, 338 quantification, see polymorphism Quest, 11, 409 ramified theory of types, 2 range of a relation, 16 rank-2 polymorphism, 359 raw type, 248 rcdsub implementation, 181–224 reachableF , 294 recon implementation, 317–338 reconbase implementation, 330 reconstruction, see type reconstruction record kinds, 445 records, 129–131 Cardelli-Mitchell calculus, 207 Church encoding, 396–400 concatenation, 207 row variables, 208, 337 recursion, 65–66, 142–145 fixed-point combinator, 65 polymorphic, 338 recursive types, 253, 267–280 Amadio-Cardelli algorithm, 309–311 and subtyping, 279 equi-recursive vs. iso-recursive, 275 history, 279–280 in ML, 277–278 in nominal systems, 253 metatheory, 281–313 µ notation, 299–304 subtyping, 281–290, 298–313 type reconstruction, 313, 338 recursive values from recursive types, 273 redex, 56 reduce function, 63 reducibility candidates, 150 reduction vs. evaluation (terminology), 34 references, 153–170 allocation, 154 and subtyping, 199–200 assignment, 154 dereferencing, 154 subtyping, 198 616 Index type safety problems, 158 type safety problems with polymorphism, 335–336 refinement types, 207 reflection, 196, 252 and casting, 196 reflexive closure, 17 reflexive relation, 16 reflexivity of subtyping, 182 region inference, 8 regular trees, 298–299 relation, 15 logical, see logical relations removenames, 78 representation independence, 371 representation of numbers by Church numerals, 67 representation type (of an object), 230 restorenames, 78 row kinds, 445 row variables, 11, 208, 337, 489 rule computation, 35, 72 congruence, 35, 72 naming conventions, 565 schema, 27 rule, inference, 27 rule schema, 27 rules B-IfFalse, 43 B-IfTrue, 43 B-IszeroSucc, 43 B-IszeroZero, 43 B-PredSucc, 43 B-PredZero, 43 B-Succ, 43 B-Value, 43 CT-Abs, 322, 542 CT-AbsInf, 330 CT-App, 322, 542 CT-False, 322 CT-Fix, 543 CT-If, 322 CT-IsZero, 322 CT-LetPoly, 332 CT-Pred, 322 CT-Proj, 545 CT-Succ, 322 CT-True, 322 CT-Var, 322, 542 CT-Zero, 322 E-Abs, 502 E-App1, 72, 103, 160, 166, 186, 343, 392, 446, 450, 470, 502, 503 E-App2, 72, 103, 160, 166, 186, 343, 392, 446, 450, 470, 502 E-AppAbs, 72, 81, 103, 160, 166, 186, 342, 343, 392, 446, 450, 470, 502, 503 E-AppErr1, 172 E-AppErr2, 172 E-AppRaise1, 175 E-AppRaise2, 175 E-Ascribe, 122, 194 E-Ascribe1, 122 E-AscribeEager, 123 E-Assign, 161, 166 E-Assign1, 161, 166 E-Assign2, 161, 166 E-Case, 132, 136 E-CaseInl, 132, 135 E-CaseInr, 132, 135 E-CaseVariant, 136 E-Cast, 258 E-CastNew, 258 E-Cons1, 147 E-Cons2, 147 E-Deref, 161, 166 E-DerefLoc, 161, 166 E-Downcast, 195 E-Field, 258 E-Fix, 144 E-FixBeta, 144 E-Fld, 276 E-Funny1, 40 E-Funny2, 40 E-GC, 514 E-Head, 147 Index E-HeadCons, 147 E-If, 34 E-If-Wrong, 42 E-IfFalse, 34 E-IfTrue, 34 E-Inl, 132, 135 E-Inr, 132, 135 E-Invk-Arg, 258 E-Invk-Recv, 258 E-InvkNew, 258 E-Isnil, 147 E-IsnilCons, 147 E-IsnilNil, 147 E-IsZero, 41 E-IsZero-Wrong, 42 E-IszeroSucc, 41 E-IszeroZero, 41 E-Let, 124, 131, 335 E-LetV, 124, 131, 332 E-New-Arg, 258 E-Pack, 366, 452 E-Pair1, 126 E-Pair2, 126 E-PairBeta1, 126 E-PairBeta2, 126 E-Pred, 41 E-Pred-Wrong, 42 E-PredSucc, 41, 48 E-PredZero, 41 E-Proj, 128, 129, 187 E-Proj1, 126 E-Proj2, 126 E-ProjNew, 258 E-ProjRcd, 129, 187, 201, 484 E-ProjTuple, 128 E-Raise, 175 E-RaiseRaise, 175 E-Rcd, 129, 187, 484 E-Ref, 162, 166 E-RefV, 162, 166 E-Seq, 120 E-SeqNext, 120 E-Succ, 41 E-Succ-Wrong, 42 617 E-Tail, 147 E-TailCons, 147 E-TApp, 343, 392, 450, 470 E-TappTabs, 342, 343, 385, 392, 450, 470 E-Try, 174, 175 E-TryError, 174 E-TryRaise, 175 E-TryV, 174, 175 E-Tuple, 128 E-Typetest1, 195 E-Typetest2, 195 E-Unfld, 276 E-UnfldFld, 276 E-Unpack, 366 E-UnpackPack, 366, 367, 452 E-UpdateV, 484 E-Variant, 136 E-Wildcard, 507 K-Abs, 446, 450, 470 K-All, 450, 470 K-App, 446, 450, 470 K-Arrow, 446, 450, 470 K-Some, 452 K-Top, 470 K-TVar, 446, 450, 470 M-Rcd, 131 M-Var, 131 P-Rcd, 509 P-Rcd’, 509 P-Var, 509 Q-Abs, 446, 451, 471 Q-All, 451, 471 Q-App, 446, 451, 471 Q-AppAbs, 441, 446, 451, 471 Q-Arrow, 446, 451, 471 Q-Refl, 446, 451, 471 Q-Some, 452 Q-Symm, 446, 451, 471 Q-Trans, 446, 451, 471 QR-Abs, 454 QR-All, 454 QR-App, 454 QR-AppAbs, 454 618 Index QR-Arrow, 454 QR-Refl, 454 S-Abs, 468, 471 S-All, 392, 394, 395, 427, 471 S-Amber, 311 S-App, 468, 471 S-Array, 198 S-ArrayJava, 198 S-Arrow, 184, 186, 211, 392, 471 S-Assumption, 311 S-Bot, 192 S-Eq, 468, 471 S-Inter1, 206 S-Inter2, 206 S-Inter3, 206 S-Inter4, 206 S-List, 197 S-ProdDepth, 187 S-ProdWidth, 187 S-Rcd, 211 S-RcdDepth, 183, 187, 484 S-RcdPerm, 184, 187 S-RcdVariance, 484 S-RcdWidth, 183, 187, 484 S-Ref, 198 S-Refl, 182, 186, 211, 392 S-RefSink, 199 S-RefSource, 199 S-Sink, 199 S-Some, 406, 476, 556 S-Source, 199 S-Top, 185, 186, 211, 392, 471 S-Trans, 183, 186, 209, 211, 392, 471 S-TVar, 392, 394, 471 S-VariantDepth, 197 S-VariantPerm, 197 S-VariantWidth, 197 SA-All, 422, 424 SA-Arrow, 212, 422, 424 SA-Bot, 220 SA-Rcd, 212 SA-Refl-TVar, 422, 424 SA-Top, 212, 422, 424 SA-Trans-TVar, 422, 424 T-Abs, 101, 103, 167, 186, 343, 392, 447, 451, 471 T-App, 102, 103, 167, 181, 186, 343, 392, 447, 451, 471 T-Ascribe, 122, 194 T-Assign, 159, 165, 167, 199 T-Case, 132, 136 T-Cast, 530 T-Cons, 147 T-DCast, 259 T-Deref, 159, 165, 167, 199 T-Downcast, 194 T-Eq, 441, 447, 451 T-Error, 172 T-Exn, 175 T-False, 93 T-Field, 259 T-Fix, 144 T-Fld, 276 T-Head, 147 T-If, 93, 102, 218 T-Inl, 132, 135 T-Inr, 132, 135 T-Invk, 259 T-Isnil, 147 T-IsZero, 93 T-Let, 124, 332, 509 T-LetPoly, 332, 333 T-Loc, 164, 167 T-New, 259 T-Nil, 147 T-Pack, 365, 366, 406, 452 T-Pair, 126 T-Pred, 93 T-Proj, 128, 129, 187, 484 T-Proj1, 126 T-Proj2, 126 T-Rcd, 129, 187, 484 T-Ref, 159, 165, 167 T-SCast, 259 T-Seq, 120 T-Sub, 182, 186, 209, 392, 471 T-Succ, 93 Index T-TAbs, 342, 343, 392, 395, 451, 471 T-Tail, 147 T-TApp, 342, 343, 392, 395, 451, 471 T-True, 93 T-Try, 174, 175 T-Tuple, 128 T-Typetest, 195 T-UCast, 259 T-Unfld, 276 T-Unit, 119, 167 T-Unpack, 366, 406, 435, 452 T-Update, 484 T-Var, 101, 103, 167, 186, 259, 343, 392, 447, 451, 471 T-Variant, 136, 197 T-Wildcard, 507 T-Zero, 93 TA-Abs, 217, 419 TA-App, 217, 419 TA-AppBot, 220 TA-If, 220, 526 TA-Proj, 217 TA-ProjBot, 220 TA-Rcd, 217 TA-TAbs, 419 TA-TApp, 419 TA-Unpack, 436 TA-Var, 217, 419 XA-Other, 418 XA-Promote, 418 run-time code generation, 109 run-time error, 42 trapped vs. untrapped, 7 run-time monitoring, 1 safety, 3, 6–8, 95–98 problems with references, 158 problems with references and polymorphism, 335–336 satisfaction of a constraint set by a substitution, 321 saturated sets, 150 Scheme, 2, 6, 8, 45 units, 368 scope, 55 619 scoping of type variables, 393–394 second-order lambda-calculus, 341, 461 security, type systems and, 9 self, 227, 234–244, 486–488 semantics alternative styles, 32–34 axiomatic, 33 denotational, 33 operational, 32 semi-unification, 338 semistructured databases, 207 sequences, basic notations, 18 sequencing notation, 119–121 and references, 155 sets, basic operations on, 15 sharing, 445, 465 shifting (of nameless terms), 78–80 ML implementation, 85–87 side effects, 153 simple theory of types, 2 simple types, 100 simplebool implementation, 113–116 simply typed lambda-calculus, 2, 11, 99–111 extensions, 117–146 ML implementation, 113–116 pure, 102 with type operators, 445 Simula, 11, 207 single-field variant, 138–140 singleton kinds, 441, 445, 465 size of a term, 29 small-step operational semantics, 32, 42 Smalltalk, 226 soundness, see safety soundness and completeness, 212 of algorithmic subtyping, 423 of constraint typing, 325 Source and Sink constructors, 199 spurious subsumption, 253 Standard ML, xvii, 7, 45 statement, 36 static distance, 76 620 Index static vs. dynamic typing, 2 store, 153 store typing, 162–165 stratified polymorphism, 360 streams, 270–271 strict vs. non-strict evaluation, 57 String type, 117 strong binary operations, 376 strong normalization, 152, 353 structural operational semantics, 32, 34 structural unfolding, 489 structural vs. nominal type systems, 251–254 stuck term, 41 stupid cast, 259–260 subclass, 227, 232 subexpressions of µ-types, 304–309 subject expansion, 98, 108 subject reduction, see preservation subscripting conventions, 566 subset semantics of subtyping, 182, 201–202 substitution, 69–72, 75–81, 83–88 capture-avoiding, 70 ML implementation, 85–87 type-, 317 substitution lemma, 106, 168, 189, 453 substitution on types, 342 ML implementation, 382 subsumption, 181–182 postponement of, 214 subtraction of Church numerals, 62 subtype polymorphism, see subtyping subtyping, 181–224, see also bounded quantification Top and Bot types, 191–193 algorithm, 209–213, 417–436 algorithmic, in nominal systems, 253 and ascription, 193–196 and base types, 200 and channel types, 200 and objects, 227 and references, 199–200 and type reconstruction, 338, 355 and variant types, 196–197 arrays, 198–199 coercion semantics, 200–206 depth, 183 higher-order, 11, 467–473 intersection types, 206–207 iso-recursive types, 311–312 joins and meets in System F<: , 432– 435 lists, 197 ML implementation, 221–224 objects, 229–230 positive, 489 power types, 472 record permutation, 184 recursive types, 279, 281–290, 298– 313 references, 198 reflexivity, 182 subset semantics, 182, 201–202 subtype relation, 182–187 transitivity, 183 type operators, 467–473 undecidability of System F<: , 427– 431 union types, 206–207 vs. other forms of polymorphism, 341 width, 183 sum types, 132–135 super, 234 supertype, 182 support, 290 surface syntax, 53 syllabi for courses, xvii symmetric relation, 16 syntactic control of interference, 170 syntactic sugar, 121 syntax, 26–29, 52–55, 69 ML implementation, 46–47, 383–385 syntax-directedness, 209 System F, 11, 339–361 fragments, 358–359 history, 341 Index ML implementation, 381–387 System Fω , 449–466 and higher-order logic, 109 fragments, 461 System Fω <: , 467–473 System F<: , 389–409 kernel and full variants, 391 System λω , 445–447 T , see terms tag, type-, 2 tag-free garbage collection, 341 tagged representation of atomic values, 201 tagging creating new types by, 133 tail recursion, 296 TAL, 11 Tarski-Knaster fixed point theorem, 283 termination measure, 39 terminology, reduction vs. evaluation, 34 terms, 24, 26 and expressions (terminology), 24 closed, 55 depth, 29 induction on, 29–32 inductive definition of (nameless form), 77 ML implementation, 46, 83–85 nameless form, see de Bruijn indices size, 29 stuck, 41 theorem proving, types in, 9, 464 this, see self thunk, 239 TinkerType, xx Titanium, 8 Top type, 185, 191–193 top-down subexpressions of a recursive type, 304 Top[K], 468 total function, 16 total order, 17 transitive closure, 17, 289 621 transitive relation, 16 transitivity and coinduction, 288–290 transitivity of subtyping, 183 translucent types, 11 trapped vs. untrapped errors, 7 tree, 538 abstract syntax, 25 derivation, 36 regular, 298–299 type, 285 treeof, 300 tuples, 126–129 two-counter machines, 430 tyarith implementation, 91–98 typability, 93, 109–110, 354–357 type abstraction, 342 type annotations, 3, 10, 111 type application, 342 type classes, 337, 338 type constructors, see type operators type destructors, 489 type environment, 101 type equivalence, 447, 453–456 type erasure, 110, 354 type errors, 3 finding, 545 type exposure, 417–418 type inference, see type reconstruction type names, 251 type operators, 100, 439–447 bounded, 473 co- and contravariant, 473 definition equivalence, 441 in nominal systems, 254 quantification over, 449–466 subtyping, 467–473 type reconstruction, 317–338, 354–357 colored local type inference, 355 greedy, 355 history, 336–338 local type inference, 355 recursive types, 313, 338 subtyping, 338, 355 type safety, see safety 622 Index type scheme, 359 type substitution, 317 ML implementation, 382 type systems and efficiency, 8 and portability, 7 and security, 9 and theorem provers, 9, 464 applications, 8–9 as formal methods, 1 category theory and, 12 defined, 1–4 history, 10 in mathematics and logic, 2 language design and, 9–10 role in computer science, 1–4 type tags, 2, 196, 252 type theory, see type systems constructive, 2 type variables, 319–320 type-assignment systems, 101 type-directed partial evaluation, 152 type-erasure semantics, 357 type-passing semantics, 357 typecase, 341 typed arithmetic expressions, 91–98 typed assembly language, 11 typed intermediate languages, 11 typed lambda-calculi, 2 types, 92 typing context, 101 typing derivations, 94 desugaring of, 125 semantics defined on, 111, 200–206 typing relation, 92–95, 100–103 algorithm, 213–218 ML implementation, 113–116 properties, 104–108 undecidability of full type reconstruction for System F, 354 of partial type reconstruction for System F, 354 of subtyping for System F<: , 427– 431 undefinedness vs. failure, 16 unification, 321, 326–329 union types, 142, 206–207 disjoint, 142 uniqueness of normal forms, 39 uniqueness of types, 94, 104, 511 and annotations, 135, 141 and sums, 134–135 Unit type, 118–119 unit value, 118–119 units (in Scheme), 368 universal domain, 273 universal set, 282 universal types, 339–361 unsafe declarations, 7 untyped implementation, 83–88 untyped arithmetic expressions, 23–44 untyped lambda-calculus, 11, 51–73 representation using recursive types, 273–275 up-cast, see casting update, polymorphic, 482–485 value, 34, 57 numeric, 40 value restriction, 336, 358 variable capture, 70 variables bound, 55, 69–72 free, 55 variant types, 132–142 and subtyping, 196–197 extensible, 177 single-field, 138–140 vs. datatypes, 140–142 weak binary operations, 375 weak head reduction, 460 weak pointers, 515 weak type variable, 336 weakening lemma, 106 web resources, xx well-formed context, 459 Index well-founded order, 18 set, 18 well-typed term, 93 width subtyping, 183 wildcard bindings, 119–121 witness type, 364 wrong, 42, 73 XML, 9, 207, 313 Y combinator, 65 Year 2000 problem, 9 Z combinator, 65 623

 

pages: 448 words: 71,301

Programming Scala by Unknown

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

domain-specific language, en.wikipedia.org, fault tolerance, general-purpose programming language, loose coupling, type inference, web application

For dynamically typed languages, the tests must cover possible type errors, too. If you are coming from a dynamically typed language, you may find that your test suites are a little smaller as a result, but not that much smaller. Many developers who find static languages too verbose often blame static typing for the verbosity when the real problem is a lack of type inference. In type inference, the compiler infers the types of values based on the context. For example, the compiler will recognize that x = 1 + 3 means that x must be an integer. Type inference reduces verbosity significantly, making the code feel more like code written in a dynamic language. We have worked with both static and dynamic languages, at various times. We find both kinds of languages compelling for different reasons. We believe the modern software developer must master a range of languages and tools.

It can be of type HashMap for all we care: import java.util.Map import java.util.HashMap ... val intToStringMap2 = new HashMap[Integer, String] This declaration requires no type annotations on the lefthand side because all of the type information needed is on the righthand side. The compiler automatically makes intToStringMap2 a HashMap[Integer,String]. Type inference is used for methods, too. In most cases, the return type of the method can be inferred, so the : and return type can be omitted. However, type annotations are required for all method parameters. Pure functional languages like Haskell (see, e.g., [O’Sullivan2009]) use type inference algorithms like Hindley-Milner (see [Spiewak2008] for an easily digested explanation). Code written in these languages require type annotations less often than in Scala, because Scala’s type inference algorithm has to support object-oriented typing as well as functional typing. So, Scala requires more type annotations than languages like Haskell. Here is a summary of the rules for when explicit type annotations are required in Scala.

[Szyperski1998] Clemens Szyperski, Component Software: Beyond Object-Oriented Programming, Addison-Wesley Longman Limited, 1998. [TDD] Test-Driven Development, http://en.wikipedia.org/wiki/Test-driven_develop ment. [Terracotta] Terracotta, http://terracotta.org/. [TestNG] TestNG, http://testng.org/. [Turbak2008] Franklyn Turbak, David Gifford, and Mark A. Sheldon, Design Concepts of Programming Languages, The MIT Press, 2008. [TypeInference] Type inference, http://en.wikipedia.org/wiki/Type_inference. [VanRoy2004] Peter Van Roy and Seif Haridi, Concepts, Techniques, and Models of Computer Programming, The MIT Press, 2004. [Wampler2008] Dean Wampler, Traits vs. Aspects in Scala, http://blog.objectmentor .com/articles/2008/09/27/traits-vs-aspects-in-scala. References | 391 Download at WoweBook.Com [WirfsBrock2003] Rebecca Wirfs-Brock and Alan McKean, Object Design: Roles, Responsibilities, and Collaborations, Pearson Education, 2003. 392 | Appendix: References Download at WoweBook.Com Glossary $tag Actor Model of Concurrency A method declared by the ScalaObject trait and used internally by Scala.

 

Scala in Action by Nilanjan Raychaudhuri

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

continuous integration, create, read, update, delete, database schema, domain-specific language, en.wikipedia.org, failed state, fault tolerance, general-purpose programming language, index card, MVC pattern, type inference, web application

Even though the return type is optional, you do have to specify the type of the parameters when defining functions. Scala type inference will figure out the type of parameters when you invoke the function but not during the function declaration.[4],[5] 4 “Type inference,” Wikipedia, http://mng.bz/32jw. 5 Daniel Spiewak, posted at Code Commit, “What is Hindley-Milner? (and why is it cool?),” undated, http://mng.bz/H4ip. Type inference If you have a background in Haskell, OCaml, or any other type of inferred programming language, the way Scala parameters are defined could feel a bit weird. The reason is that Scala doesn’t use the Hindley-Milner algorithm to infer type; instead Scala’s type inference is based on declaration-local information, also known as local type inference. Type inference is out of the scope of this book, but if you’re interested you can read about the Hindley-Milner type inference algorithm and why it’s useful.

But having constraints is useful when building a large application because they allow you to enforce a certain set of rules across the codebase. Scala, being a type-inferred language, takes care of most of the boilerplate code for the programmer (that’s what compilers are good for, right?) and takes you close to a dynamically typed language, but with all the benefits of a statically typed language. Definition Type inference is a technique by which the compiler determines the type of a variable or function without the help of a programmer. The compiler can deduce that the variable s in s="Hello" will have the type string because "hello" is a string. The type inference ensures the absence of any runtime type errors without putting a declaration burden on the programmer. To demonstrate how type inference works, create an array of maps in Scala: val computers = Array( Map("name" -> "Macbook", "color" -> "white"), Map("name" -> "HP Pavillion", "color" -> "black") ) If you run this Scala code in the Scala REPL, you’ll see the following output: computers: Array[scala.collection.immutable.Map[java.lang.String,java.lang.String]] = Array(Map(name -> Macbook, color -> white), Map(name -> HP Pavillion, color -> black)) Even though you only specified an array of maps with key and value, the Scala compiler was smart enough to deduce the type of the array and the map.

In the case of addFunction, we could replace all the calls made to it with the output value, and the behavior of the program wouldn’t change. Now let’s talk about functional programming languages. Functional programming languages that support this style of programming provide at least some of the following features: Higher-order functions (chapter 4) Lexical closures (chapter 3) Pattern matching (chapters 2 and 3) Single assignment (chapter 2) Lazy evaluation (chapter 2) Type inference (chapter 2) Tail call optimization (chapter 5) List comprehensions (chapters 2 and 4) Mondadic effects (chapter 5) Side effects A function or expression is said to have a side effect if, in addition to producing a value, it modifies some state or has an observable interaction with calling functions or the outside world. A function might modify a global or a static variable, modify one of its arguments, raise an exception, write data to a display or file, read data, or call other functions having side effects.

 

pages: 1,076 words: 67,364

Haskell Programming from first principles by Christopher Allen, Julie Moronuki

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

c2.com, en.wikipedia.org, natural language processing, spaced repetition, Turing complete, Turing machine, type inference, web application, Y Combinator

If, however, we take out the string value and replace it with another variable, see what happens: Prelude> let myGreet x y = x ++ y Prelude> :type myGreet myGreet :: [a] -> [a] -> [a] We’re back to a polymorphic type signature, the same signature for (++) itself, because the compiler has no information by which to infer the types for any of those variables (other than that they are lists of some sort). Let’s see type inference at work. Open your editor of choice and enter the following snippet: -- typeInference1.hs module TypeInference1 where f :: Num a => a -> a -> a f x y = x + y + 3 Then when we load the code into GHCi to experiment: Prelude> :l typeInference1.hs CHAPTER 5. TYPES 160 [1 of 1] Compiling TypeInference1 Ok, modules loaded: TypeInference1. Prelude> f 1 2 6 Prelude> :t f f :: Num a => a -> a -> a Prelude> :t f 1 f 1 :: Num a => a -> a Because the numeric literals in Haskell have the (typeclass constrained) polymorphic type Num a => a, we don’t get a more specific type when applying 𝑓 to 1. Look at what happens when we elide the explicit type signature for 𝑓 : -- typeInference2.hs module TypeInference2 where f x y = x + y + 3 No type signature for 𝑓 , so does it compile?

Here’s what the type signature looks like: Prelude> :type fromIntegral fromIntegral :: (Num b, Integral a) => a -> b So, it takes a value, 𝑎, of an Integral type and returns it as a value, 𝑏, of any Num type. Let’s see how that works with our fractional division problem: Prelude> 6 / fromIntegral (length [1, 2, 3]) 2.0 And now all is right with the world once again. 5.7 Type inference Haskell does not obligate us to assert a type for every expression or value in our programs because it has type inference. Type inference is an algorithm for determining the types of expressions. Haskell’s type inference is built on an extended version of the Damas-HindleyMilner type system. Haskell will infer the most generally applicable (polymorphic) type that is still correct. Essentially, the compiler starts from the values whose types it knows and then works out the types of the other values.

Look at what happens when we elide the explicit type signature for 𝑓 : -- typeInference2.hs module TypeInference2 where f x y = x + y + 3 No type signature for 𝑓 , so does it compile? Does it work? Prelude> :l typeInference2.hs [1 of 1] Compiling TypeInference2 Ok, modules loaded: TypeInference2. Prelude> :t f f :: Num a => a -> a -> a Prelude> f 1 2 6 Nothing changes. In certain cases there might be a change, usually when you are using typeclasses in a way that doesn’t make it clear which type you mean unless you assert one. Intermission: Exercises Look at these pairs of functions. One function is unapplied, so the compiler will infer maximally polymorphic type. The second function has been applied to a value, so the inferred type signature may have become concrete, or at least less polymorphic. Figure out how the type would change and why, make a note of what you think the new inferred type would be and then check your work in GHCi. CHAPTER 5.

 

pages: 754 words: 48,930

Programming in Scala by Martin Odersky, Lex Spoon, Bill Venners

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

domain-specific language, Silicon Valley, sorting algorithm, type inference, web application

On the other hand, even if that rule were relaxed, the inferencer still could not come up with a type for op because its parameter types are not given. Hence, there is a Catch-22 situation which can only be resolved by an explicit type annotation from the programmer. This example highlights some limitations of the local, flow-based type inference scheme of Scala. It is not present in the more global HindleyMilner style of type inference used in functional languages such as ML or Haskell. However, Scala’s local type inference deals much more gracefully with object-oriented subtyping than the Hindley-Milner style does. Fortunately, the limitations show up only in some corner cases, and are usually easily fixed by adding an explicit type annotation. Adding type annotations is also a useful debugging technique when you get confused by type error messages related to polymorphic methods.

On the other hand, at least one of the two annotations in the following example is annoying: val x: HashMap[Int, String] = new HashMap[Int, String]() Clearly, it should be enough to say just once that x is a HashMap with Ints as keys and Strings as values; there’s no need to repeat the same phrase twice. Scala has a very sophisticated type inference system that lets you omit almost all type information that’s usually considered annoying. In the previous example, the following two less annoying alternatives would work just as well: val x = new HashMap[Int, String]() val x: Map[Int, String] = new HashMap() Type inference in Scala can go quite far. In fact, it’s not uncommon for user code to have no explicit types at all. Therefore, Scala programs often look a bit like programs written in a dynamically typeddynamic!typing scripting language. This holds particularly for client application code, which glues together pre-written library components.

Scala is also not the first language to integrate functional and object15 The major deviation from Java concerns the syntax for type annotations—it’s “variable: Type” instead of “Type variable” in Java. Scala’s postfix type syntax resembles Pascal, Modula-2, or Eiffel. The main reason for this deviation has to do with type inference, which often lets you omit the type of a variable or the return type of a method. Using the “variable: Type” syntax this is easy—just leave out the colon and the type. But in C-style “Type variable” syntax you cannot simply leave off the type—there would be no marker to start the definition anymore. You’d need some alternative keyword to be a placeholder for a missing type (C# 3.0, which does some type inference, uses var for this purpose). Such an alternative keyword feels more ad-hoc and less regular than Scala’s approach. 16 Landin, “The Next 700 Programming Languages.” [Lan66] Cover · Overview · Contents · Discuss · Suggest · Glossary · Index 56 Section 1.5 Chapter 1 · A Scalable Language oriented programming, although it probably goes furthest in this direction.

 

pages: 184 words: 13,957

Haskell by Graham Hutton

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

Eratosthenes, John Conway, Simon Singh, type inference

For example: ¬ False :: Bool ¬ True :: Bool ¬ (¬ False) :: Bool In Haskell, every expression must have a type, which is calculated prior to evaluating the expression by a process called type inference. The key to this process is a typing rule for function application, which states that if f is a function that maps arguments of type A to results of type B , and e is an expression of type A, then the application f e has type B : 18 TYPES AND CLASSES f :: A → B e :: A f e :: B For example, the typing ¬ False :: Bool can be inferred from this rule using the fact that ¬ :: Bool → Bool and False :: Bool . On the other hand, the expression ¬ 3 does not have a type under the above rule for function application, because this would require that 3 :: Bool , which is not valid because 3 is not a logical value. Expressions such as ¬ 3 that do not have a type are said to contain a type error, and are deemed to be invalid expressions. Because type inference precedes evaluation, Haskell programs are type safe, in the sense that type errors can never occur during evaluation.

Because type inference precedes evaluation, Haskell programs are type safe, in the sense that type errors can never occur during evaluation. In practice, type inference detects a very large class of program errors, and is one of the most useful features of Haskell. Note, however, that the use of type inference does not eliminate the possibility that other kinds of error may occur during evaluation. For example, the expression 1 ‘div ‘ 0 is free from type errors, but produces an error when evaluated because division by zero is undefined. The downside of type safety is that some expressions that evaluate successfully will be rejected on type grounds. For example, the conditional expression if True then 1 else False evaluates to the number 1, but contains a type error and is hence deemed invalid. In particular, the typing rule for a conditional expression requires that both possible results have the same type, whereas in this case the first such result, 1, is a number and the second, False , is a logical value.

Although it is difficult to make an objective comparison, Haskell programs are often between two and ten times shorter than programs written in other current languages. r Powerful type system (chapters 3 and 10) Most modern programming languages include some form of type system to detect incompatibility errors, such as attempting to add a number and a character. Haskell has a type system that requires little type information from the programmer, but allows a large class of incompatibility errors in programs to be automatically detected prior to their execution, using a sophisticated process called type inference. The Haskell type system is also more powerful than most current languages, by allowing functions to be “polymorphic” and “overloaded”. r List comprehensions (chapter 5) One of the most common ways to structure and manipulate data in computing is using lists. To this end, Haskell provides lists as a basic concept in the language, together with a simple but powerful comprehension notation that constructs new lists by selecting and filtering elements from one or more existing lists.

 

pages: 184 words: 13,985

Programming in Haskell by Graham Hutton

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

Eratosthenes, John Conway, Simon Singh, type inference

For example: ¬ False :: Bool ¬ True :: Bool ¬ (¬ False) :: Bool In Haskell, every expression must have a type, which is calculated prior to evaluating the expression by a process called type inference. The key to this process is a typing rule for function application, which states that if f is a function that maps arguments of type A to results of type B , and e is an expression of type A, then the application f e has type B : 18 TYPES AND CLASSES f :: A → B e :: A f e :: B For example, the typing ¬ False :: Bool can be inferred from this rule using the fact that ¬ :: Bool → Bool and False :: Bool . On the other hand, the expression ¬ 3 does not have a type under the above rule for function application, because this would require that 3 :: Bool , which is not valid because 3 is not a logical value. Expressions such as ¬ 3 that do not have a type are said to contain a type error, and are deemed to be invalid expressions. Because type inference precedes evaluation, Haskell programs are type safe, in the sense that type errors can never occur during evaluation.

Because type inference precedes evaluation, Haskell programs are type safe, in the sense that type errors can never occur during evaluation. In practice, type inference detects a very large class of program errors, and is one of the most useful features of Haskell. Note, however, that the use of type inference does not eliminate the possibility that other kinds of error may occur during evaluation. For example, the expression 1 ‘div ‘ 0 is free from type errors, but produces an error when evaluated because division by zero is undefined. The downside of type safety is that some expressions that evaluate successfully will be rejected on type grounds. For example, the conditional expression if True then 1 else False evaluates to the number 1, but contains a type error and is hence deemed invalid. In particular, the typing rule for a conditional expression requires that both possible results have the same type, whereas in this case the first such result, 1, is a number and the second, False , is a logical value.

Although it is difficult to make an objective comparison, Haskell programs are often between two and ten times shorter than programs written in other current languages. r Powerful type system (chapters 3 and 10) Most modern programming languages include some form of type system to detect incompatibility errors, such as attempting to add a number and a character. Haskell has a type system that requires little type information from the programmer, but allows a large class of incompatibility errors in programs to be automatically detected prior to their execution, using a sophisticated process called type inference. The Haskell type system is also more powerful than most current languages, by allowing functions to be “polymorphic” and “overloaded”. r List comprehensions (chapter 5) One of the most common ways to structure and manipulate data in computing is using lists. To this end, Haskell provides lists as a basic concept in the language, together with a simple but powerful comprehension notation that constructs new lists by selecting and filtering elements from one or more existing lists.

 

Practical OCaml by Joshua B. Smith

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

cellular automata, Debian, domain-specific language, general-purpose programming language, Grace Hopper, hiring and firing, John Conway, Paul Graham, slashdot, text mining, Turing complete, type inference, web application, Y2K

Really, just typing “Hello World” into the interpreter creates this program because the string "Hello World" is evaluated and returned by the toplevel. With that in mind, the previous examples have actually been your first program. However, you probably want to interact with more than the OCaml type inference engine. WHAT IS TYPE INFERENCE? Type inference is the process by which the OCaml compiler figures out type information from your code. The compiler does this for two reasons: so that the programmer does not have to specify type information, and so that the types are used correctly. These compile-time type checks are what prevent you from using a function with the wrong type. In a language such as Python, these errors would show up only during runtime. Type inference is part of the polymorphic type checker found in ML dialects. The consequence and benefits of type are discussed in more detail in Chapter 6. OCaml uses a printf style of command to output information to stdout.

A record is a collection of labels and types. These labels must be unique within the current module so the type inference engine can infer types correctly. You will create an example record that uses the 'a distance type from the last example to demonstrate this: # type 'a part_with_length = {part_name: string; part_number: int; ➥ part_length: 'a distance };; type 'a part_with_length = { part_name : string; part_number : int; part_length : 'a distance; } This example uses two basic types, strings and ints, as well as the aggregate type distance. Now that you have the part_with_length type, you can begin to define parts. Notice that you do not have to specify that you are creating this type because the type inference engine will do it for you: # let crescent_wrench = {part_name="Left Handed Crescent Wrench";part_number=1; ➥ part_length=(Foot 1)};; val crescent_wrench : 'a part_with_length = {part_name = "Left Handed Crescent Wrench"; part_number = 1; length = Foot 1} # Mutability and Records Records can have mutable elements, which are defined with the mutable keyword.

What Is the Current State of the Art? OCaml is not a dead language; it is constantly updated and worked on by a small group of fulltime researchers and the community at large. The small but active community develops the language and the standard library. INRIA is the core of OCaml development, but OCaml is used inside academic projects the world over. The language is also being improved, with a lot of work going into the type inference engine and tools such as Camlp4. Why This Book? Apress is committed to publishing the books that programmers need, and this book is one of the few English language books available on OCaml. Now is a good time for OCaml because the focus on security and correctness of programs will only become greater. As more and more of our world runs on software, the need for safe and verifiable programming and languages will increase.

 

pages: 1,065 words: 229,099

Real World Haskell by Bryan O'Sullivan, John Goerzen, Donald Stewart, Donald Bruce Stewart

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

bash_history, database schema, Debian, distributed revision control, domain-specific language, en.wikipedia.org, Firefox, general-purpose programming language, job automation, p-value, Plutocrats, plutocrats, revision control, sorting algorithm, transfer pricing, type inference, web application, Y Combinator

A helpful analogy to understand the value of static typing is to look at it as putting pieces into a jigsaw puzzle. In Haskell, if a piece has the wrong shape, it simply won’t fit. In a dynamically typed language, all the pieces are 1×1 squares and always fit, so you have to constantly examine the resulting picture and check (through testing) whether it’s correct. Type Inference Finally, a Haskell compiler can automatically deduce the types of almost[3] all expressions in a program. This process is known as type inference. Haskell allows us to explicitly declare the type of any value, but the presence of type inference means that this is almost always optional, not something we are required to do. What to Expect from the Type System Our exploration of the major capabilities and benefits of Haskell’s type system will span a number of chapters. Early on, you may find Haskell’s types to be a chore to deal with.

showHex function, Pretty Printing a String side effects, Function Types and Purity, Be Careful of Side Effects blending C with Haskell, Be Careful of Side Effects signatures, The Type of a Function of More Than One Argument sin function, Numeric Types single quotes ('), Writing Character and String Literals single-character escape codes, Single-Character Escape Codes snd function, Functions over Lists and Tuples sockets, Basic Networking–TCP Syslog Client solution maps, Solving for Check Digits in Parallel sort function, Sequential Sorting source files, Haskell Source Files, and Writing Simple Functions–Understanding Evaluation by Example space leaks, Left Folds, Laziness, and Space Leaks, Space Leaks and Strict Evaluation–Learning to Use seq, Space Profiling spines for maps, A Brief Introduction to Maps split function, Text I/O, Supplying Random Numbers supplying random numbers, Supplying Random Numbers split-base Cabal flag, Dealing with Different Build Setups splitAt function, Working with Sublists SQL (Structured Query Language), Overview of HDBC SqlError type, Error Handling SqlValues type, SqlValue sqrt function, Numeric Types square brackets ([ ]), Lists, Useful Composite Data Types: Lists and Tuples, Exhaustive Patterns and Wild Cards, Recursive Types, Filename Matching character classes, Filename Matching exhaustive patterns, as a constructor, Exhaustive Patterns and Wild Cards lists, using, Lists recursive types and, Recursive Types type variables and, Useful Composite Data Types: Lists and Tuples -sstderr RTS option, Tuning for Performance, Collecting Runtime Statistics ST (state thread) monad, The ST Monad stack, Stacking Multiple Monad Transformers–Understanding Monad Transformers by Building One, Stacking Multiple Monad Transformers–Moving Down the Stack monad transformers, Stacking Multiple Monad Transformers–Moving Down the Stack standard module, Getting Started with ghci, the Interpreter starvation, Starvation state monads, The State Monad–Monads and Functors, Using the State Monad: Generating Random Values, Running the State Monad, Motivation: Boilerplate Avoidance, A Tiny Parsing Framework random values, generating, Using the State Monad: Generating Random Values running, Running the State Monad StateT monad transformer, Stacking Multiple Monad Transformers, Transformer Stacking Order Is Important transformer stacking order and, Transformer Stacking Order Is Important static types, Static Types stderr function, Standard Input, Output, and Error stdin function, Standard Input, Output, and Error stdout function, Standard Input, Output, and Error STM (software transactional memory), Software Transactional Memory–Using Invariants, STM and Safety I/O (input/output), STM and Safety strict evaluation, Lazy Evaluation, Space Leaks and Strict Evaluation–Learning to Use seq strict types, Efficient File Processing strictness, Strictness and Tail Recursion–Understanding Core string function, Pretty Printing a String string literals, Writing Character and String Literals String type, First Steps with Types, hGetContents, Efficient File Processing, Mixing and Matching String Types file processing and, Efficient File Processing hGetContents function and, hGetContents regular expressions, Mixing and Matching String Types strings, Strings and Characters, Passing String Data Between Haskell and C–Matching on Strings, Matching on Strings, Multiline String Literals multiline literals, Multiline String Literals passing data between C and Haskell, Passing String Data Between Haskell and C–Matching on Strings, Matching on Strings matching on, Matching on Strings strong types, Strong Types struct keyword (C/C++), The structure structural recursion, Explicit Recursion Structured Query Language (SQL), Overview of HDBC structures, Defining a New Data Type, The structure, Association Lists (see also data structures) stub versions of types/functions, Developing Haskell Code Without Going Nuts subtraction (-) option, Numeric Types subtype polymorphism, Polymorphism in Haskell suffixes function, Code Reuse Through Composition sum types, Generating Test Data synchronizing variable, Simple Communication Between Threads synonyms (types), Type Synonyms syntactic sugar, Desugaring of do Blocks syslog, Basic Networking System.Cmd module, Running External Programs System.Directory library, Deleting and Renaming Files System.Directory module, Making Use of Our Pattern Matcher, Directory and File Information, File Modification Times System.Environment module, Runtime Options System.Exit module, Program Termination System.FilePath module, Making Use of Our Pattern Matcher, A Naive Finding Function System.IO library, Working with Files and Handles, Standard Input, Output, and Error, Sizing a File Safely errors, Standard Input, Output, and Error files, sizing safely, Sizing a File Safely System.IO.Error module, I/O Exceptions System.Posix module, Predicates: From Poverty to Riches, While Remaining Pure System.Posix.Files module, File Modification Times System.Random module, Using the State Monad: Generating Random Values, Supplying Random Numbers supplying random numbers, Supplying Random Numbers System.Time module, ClockTime and CalendarTime System.Win32 module, Predicates: From Poverty to Riches, While Remaining Pure systems programming, Systems Programming in Haskell–Final Words on Pipes, Dates and Times–Extended Example: Piping dates and times, Dates and Times–Extended Example: Piping T \t (tab) character, Strings and Characters, A Note About Tabs Versus Spaces vs. spaces, A Note About Tabs Versus Spaces tab (\t) character, Strings and Characters, A Note About Tabs Versus Spaces vs. spaces, A Note About Tabs Versus Spaces tables (hash), Life Without Arrays or Hash Tables, Maps, Hashing Values, Turning Two Hashes into Many maps and, Maps turning two into many, Turning Two Hashes into Many tail function, Useful Composite Data Types: Lists and Tuples, Functions over Lists and Tuples, Recursion, Basic List Manipulation tail recursion, Strictness and Tail Recursion tails function, As-patterns, Code Reuse Through Composition suffixes function and, Code Reuse Through Composition take function, Functions over Lists and Tuples takeWhile function, Working with Sublists tan function, Numeric Types TCP, communicating with, Communicating with TCP–TCP Syslog Client templates (C++), Parameterized Types temporary files, Temporary Files Ternary type, Generating Test Data testing, Testing and Quality Assurance (see quality assurance) text, Warming Up: Portably Splitting Lines of Text–Infix Functions, Text I/O–Filename Matching, Escaping Text escaping, Escaping Text I/O (input/output), Text I/O–Filename Matching splitting lines of, Warming Up: Portably Splitting Lines of Text–Infix Functions text I/O, Text I/O–Filename Matching “text mode”, reading files, Warming Up: Portably Splitting Lines of Text Text.Regex.Posix module, Regular Expressions in Haskell then and else branches, Conditional Evaluation thread maps, The Main Thread and Waiting for Other Threads -threaded compiler option, Using Multiple Cores with GHC threaded runtime, Using Multiple Cores with GHC threads, Concurrent Programming with Threads, Simple Communication Between Threads, The Main Thread and Waiting for Other Threads–Communicating over Channels, Finding the Status of a Thread, Communication Between Threads communication between, Simple Communication Between Threads, Communication Between Threads finding status of, Finding the Status of a Thread waiting for other threads, The Main Thread and Waiting for Other Threads–Communicating over Channels throw function, Throwing Exceptions thunks, Lazy Evaluation TimeDiff type, TimeDiff for ClockTime times, Dates and Times–Extended Example: Piping, File Modification Times file modifications and, File Modification Times .tix files, Measuring Test Coverage with HPC toCalendarTime function, Using CalendarTime toInteger function, Numeric Types top level names, Introducing Local Variables toRational function, Numeric Types total functions, Partial and Total Functions toUpper function, Transforming Every Piece of Input toUTCTime function, Using CalendarTime transactions (database), Transactions transformer stacking, Transformer Stacking Order Is Important traverse function, Controlling Traversal, Density, Readability, and the Learning Process, Another Way of Looking at Traversal readability of, Density, Readability, and the Learning Process triple (3-tuple), Useful Composite Data Types: Lists and Tuples True Boolean value, Boolean Logic, Operators, and Value Comparisons truncate function, Representing JSON Data in Haskell, Numeric Types try keyword, Lookahead, First Steps with Exceptions, I/O Exceptions exceptions and, First Steps with Exceptions, I/O Exceptions I/O (input/output), I/O Exceptions tuples, Useful Composite Data Types: Lists and Tuples–Functions over Lists and Tuples, Functions over Lists and Tuples, Tuples, Algebraic Data Types, and When to Use Each algebraic data types and, Tuples, Algebraic Data Types, and When to Use Each functions for, Functions over Lists and Tuples two-dimensional arrays, Folding over Arrays two-dimensional vectors, Tuples, Algebraic Data Types, and When to Use Each :type command, First Steps with Types, Defining a New Data Type type constructors, Defining a New Data Type, Looking for Shared Patterns, Almost a State Monad Monads and, Looking for Shared Patterns, Almost a State Monad type inference, Type Inference, Type Inference Is a Double-Edged Sword–A More General Look at Rendering type keyword, Type Synonyms type signatures, Some Common Basic Types type variables, Useful Composite Data Types: Lists and Tuples, Polymorphism in Haskell polymorphism and, Polymorphism in Haskell type-based testing, QuickCheck: Type-Based Testing Typeable typeclass, Dynamic Exceptions typeclasses, Static Types, Using Typeclasses–Conclusion, Declaring Typeclass Instances, Important Built-in Typeclasses–Automatic Derivation, Automatic Derivation, Living in an Open World–How to Give a Type a New Identity, Relaxing Some Restrictions on Typeclasses, The Dreaded Monomorphism Restriction–Conclusion, Using Typeclasses, More Typeclass Instances automatic derivation, Automatic Derivation built-in, Important Built-in Typeclasses–Automatic Derivation declaring instances, Declaring Typeclass Instances instances, More Typeclass Instances monomorphism restriction, The Dreaded Monomorphism Restriction–Conclusion open world assumptions, Living in an Open World–How to Give a Type a New Identity restrictions, relaxing, Relaxing Some Restrictions on Typeclasses using, Using Typeclasses typed pointers, Typed Pointers types, First Steps with Types–A Simple Program, Why Care About Types?

Several Haskell compression libraries exist, all of which have simple interfaces: a compression function accepts an uncompressed string and returns a compressed string. We can use function composition to render JSON data to a string, and then compress to another string, postponing any decision on how to actually display or transmit the data. Type Inference Is a Double-Edged Sword A Haskell compiler’s ability to infer types is powerful and valuable. Early on, you’ll probably face a strong temptation to take advantage of type inference by omitting as many type declarations as possible. Let’s simply make the compiler figure the whole lot out! Skimping on explicit type information has a downside, one that disproportionately affects new Haskell programmers. As such a programmer, we’re extremely likely to write code that will fail to compile due to straightforward type errors.

 

Functional Programming in Scala by Paul Chiusano, Rúnar Bjarnason

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

domain-specific language, iterative process, loose coupling, sorting algorithm, type inference, web application

Again, notice these functions take time proportional only to the number of elements being dropped—we do not need to make a copy of the entire List. Footnote 10mdropWhile has two argument lists to improve type inference. See sidebar. www.it-ebooks.info 41 def drop[A](l: List[A], n: Int): List[A] def dropWhile[A](l: List[A])(f: A => Boolean): List[A] SIDEBAR Type inference in Scala When writing functions like dropWhile, we will often place the List in the first argument group, and any functions, f that receive elements of the List in a later argument group. We can call this function with two sets of parentheses, like dropWhile(xs)(f), or we can partially apply it by supplying only the first argument dropWhile(xs). This returns a function that accepts the other argument, f. The main reason for grouping the arguments this way is to assist with type inference. If we do this, Scala can determine the type of f without any annotation, based on what it knows about the type of the List, which makes the function more convenient to use, especially when passing a function literal like x => x > 34 in for f, which would otherwise require an annotation like (x: Int) => x > 34.

Putting this all together for this case, our function will take as arguments the value to return in the case of the empty list, and the function to add an element to the result in the case of a nonempty list:12 Footnote 12mIn the Scala standard library, foldRight is a method on List and its arguments are curried similarly for better type inference. Listing 3.3 Right folds and simple uses def foldRight[A,B](l: List[A], z: B)(f: (A, B) => B): B = l match { case Nil => z case Cons(x, xs) => f(x, foldRight(xs, z)(f)) } def sum2(l: List[Int]) = foldRight(l, 0.0)(_ + _) def product2(l: List[Double]) = foldRight(l, 1.0)(_ * _) Again, placing f in its own argument group after l and z lets type inference determine the input types to f. See earlier sidebar. foldRight is not specific to any one type of element, and the value that is returned doesn't have to be of the same type as the elements either. One way of describing what foldRight does is that it replaces the constructors of the list, Nil and Cons with z and f , respectively.

Nothing is a subtype of all types, which means that in conjunction with the variance annotation, Nil can be considered a List[Int], a List[Double], and so on, exactly as we want. These concerns about variance are not very important for the present discussion and are more of an artifact of how Scala encodes data constructors via subtyping, so don't worry if this is not completely clear right now.3 Footnote 3mIt is certainly possible to write code without using variance annotations at all, and function signatures are sometimes simpler (while type inference often gets worse). Unless otherwise noted, we will be using variance annotations throughout this book, but you should feel free to experiment with both approaches. 3.2.1 Pattern matching Let's look in detail at the functions sum and product, which we place in the object List, sometimes called the companion object to List (see sidebar). Both these definitions make use of pattern matching. def sum(ints: List[Int]): Int = ints match { case Nil => 0 case Cons(x,xs) => x + sum(xs) } def product(ds: List[Double]): Double = ds match { case Nil => 1.0 case Cons(0.0, _) => 0.0 case Cons(x, xs) => x * product(xs) } As you might expect, the sum function states that the sum of an empty list is 0, www.it-ebooks.info 37 and the sum of a nonempty list is the first element, x , plus the sum of the remaining elements, xs.4 Likewise the product definition states that the product of an empty list is 1.0, the product of any list starting with 0.0 is 0.0,5 and the product of any other nonempty list is the first element multiplied by the product of the remaining elements.

 

pages: 1,201 words: 233,519

Coders at Work by Peter Seibel

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

Ada Lovelace, bioinformatics, cloud computing, Conway's Game of Life, domain-specific language, fault tolerance, Fermat's Last Theorem, Firefox, George Gilder, glass ceiling, HyperCard, information retrieval, loose coupling, Menlo Park, Metcalfe's law, premature optimization, publish or perish, random walk, revision control, Richard Stallman, rolodex, Saturday Night Live, side project, slashdot, speech recognition, the scientific method, Therac-25, Turing complete, Turing machine, Turing test, type inference, Valgrind, web application

Peyton Jones: It is, but it's much more explicit. In the original source, lots of type inference is going on and the source language is carefully crafted so that type inference is possible. In the intermediate language, the type system is much more general, much more expressive because it's more explicit: every function argument is decorated with its type. There's no type inference, there's just type checking for the intermediate language. So it's an explicitly typed language whereas the source language is implicitly typed. Type inference is based on a carefully chosen set of rules that make sure that it just fits within what the type inference engine can figure out. If you transform the program by a source-to-source transformation, maybe you've now moved outside that boundary. Type inference can't reach it any more. So that's bad for an optimization.

You lose something when the academics are all off chasing NSF grants every year. The other thing is, you see the rise in dynamic languages. You see crazy, idiotic statements about how dynamic language are going to totally unseat Java and static languages, which is nonsense. But the academics are out there convinced static type systems are the ultimate end and they're researching particular kinds of static type systems like the ML, Hindley-Milner type inferences and it's completely divorced from industry. Seibel: Why is that? Because it's not solving any real problems or because it's only a partial solution? Eich: We did some work with SML New Jersey to self-host the reference implementation of JavaScript, fourth edition, which is now defunct. We were trying to make a definitional interpreter. We weren't even using Hindley-Milner. We would annotate types and arguments to avoid these crazy, notorious error messages you get when it can't unify types and picks some random source code to blame and it's usually the wrong one.

So that's bad for an optimization. You don't want optimizations to have to worry about whether you might have just gone out of the boundaries of type inference. Seibel: So that points out that there are programs that are correct, because you're assuming a legitimate source-to-source transformation, which, if you had written it by hand, the compiler would have said, “I'm sorry; I can't type this.” Peyton Jones: Right. That's the nature of static type systems—and why dynamic languages are still interesting and important. There are programs you can write which can't be typed by a particular type system but which nevertheless don't “go wrong” at runtime, which is the gold standard—don't segfault, don't add integers to characters. They're just fine. Seibel: So when advocates of dynamic and static typing bicker the dynamic folks say, “Well, there are lots of those programs—static typing gets in the way of writing the program I want to write.”

 

pages: 496 words: 70,263

Erlang Programming by Francesco Cesarini

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

cloud computing, fault tolerance, finite state, loose coupling, revision control, RFC: Request For Comment, sorting algorithm, Turing test, type inference, web application

Trace BIFs, the dbg Tracer, and Match Specifications . . . . . . . . . . . . . . . . . . . . . . . . 355 Introduction The Trace BIFs Process Trace Flags Inheritance Flags Garbage Collection and Timestamps Tracing Calls with the trace_pattern BIF The dbg Tracer Getting Started with dbg Tracing and Profiling Functions Tracing Local and Global Function Calls Distributed Environments Redirecting the Output Match Specifications: The fun Syntax Generating Specifications Using fun2ms Difference Between ets and dbg Match Specifications Match Specifications: The Nuts and Bolts 355 357 358 360 361 362 365 366 369 369 371 371 374 375 382 383 Table of Contents | ix The Head Conditions The Specification Body Saving Match Specifications Further Reading Exercises 383 384 387 390 391 392 18. Types and Documentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 395 Types in Erlang An Example: Records with Typed Fields Erlang Type Notation TypEr: Success Types and Type Inference Dialyzer: A DIscrepancy AnaLYZer for ERlang Programs Documentation with EDoc Documenting usr_db.erl Running EDoc Types in EDoc Going Further with EDoc Exercises 395 395 396 399 401 402 403 405 407 408 410 19. EUnit and Test-Driven Development . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 411 Test-Driven Development EUnit How to Use EUnit Functional Testing, an Example: Tree Serialization The EUnit Infrastructure Assert Macros Test-Generating Functions EUnit Test Representation Testing State-Based Systems Fixtures: Setup and Cleanup Testing Concurrent Programs in Erlang Exercises 411 412 413 413 416 416 416 417 418 418 419 420 20.

.‖ Types are determined at runtime, as is the viability of the operation you ‡ Variables can also begin with an underscore; these play a role in pattern matching and are discussed in the section “Pattern Matching” on page 33. § We cover side effects and destructive operations later in the book. ‖ Other languages can avoid variable declarations for other reasons. Haskell, for instance, uses a type inference algorithm to deduce types of variables. 30 | Chapter 2: Basic Erlang are trying to execute on the variable. The following code attempting to multiply an atom by an integer will compile (with compiler warnings), but will result in a runtime error when you try to execute it: Var = one, Double = Var * 2 At first, using variables that start with capital letters might feel counterintuitive, but you’ll get used to it quickly.

Writing the following would have the same effect: -spec(create_tables(string()) -> {ok, ref()} | {error, atom()}). However, including the parameter name—assuming it is chosen to reflect its purpose— improves the documentation.* * The EDoc system described later in the chapter will automatically include parameter names in its generated type documentation even if they do not appear in the –spec statement. 398 | Chapter 18: Types and Documentation TypEr: Success Types and Type Inference The TypEr system, built by Tobias Lindahl and Kostis Sagonas,† is used to check the validity of –spec annotations, as well as to infer the types of functions in modules without type annotations. You use TypEr from the command line. You can see the full range of options by typing: typer --help Taking the example of the mobile user database from Chapter 10, the following command: typer --show usr.erl usr_db.erl gives the following output (shortened for brevity): Unknown functions: [{ets,safefixtable,2}] %% File: "usr.erl" %% ---------------spec start() -> 'ok' | {'error','starting'}.

 

pages: 559 words: 130,949

Learn You a Haskell for Great Good!: A Beginner's Guide by Miran Lipovaca

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

fault tolerance, loose coupling, type inference

This means that when you compile your program, the compiler knows which piece of code is a number, which is a string, and so on. Static typing means that a lot of possible errors can be caught at compile time. If you try to add together a number and a string, for example, the compiler will whine at you. Haskell uses a very good type system that has type inference. This means that you don’t need to explicitly label every piece of code with a type, because Haskell’s type system can intelligently figure it out. For example, if you say a = 5 + 4, you don’t need to tell Haskell that a is a number—it can figure that out by itself. Type inference makes it easier for you to write code that’s more general. If you write a function that takes two parameters and adds them together, but you don’t explicitly state their type, the function will work on any two parameters that act like numbers. Haskell is elegant and concise.

In Haskell, every expression’s type is known at compile time, which leads to safer code. If you write a program that tries to divide a Boolean type with a number, it won’t compile. This is good because it’s better to catch those kinds of errors at compile time, rather than having your program crash later on. Everything in Haskell has a type, so the compiler can reason quite a lot about your program before compiling it. Unlike Java or Pascal, Haskell has type inference. If we write a number, for example, we don’t need to tell Haskell it’s a number, because it can infer that on its own. So far, we’ve covered some of the basics of Haskell with only a very superficial glance at types, but understanding the type system is a very important part of learning Haskell. Explicit Type Declaration We can use GHCi to examine the types of some expressions. We’ll do that by using the :t command which, followed by any valid expression, tells us its type.

No value can have a type of just Maybe, because that’s not a type—it’s a type constructor. In order for this to be a real type that a value can be part of, it must have all its type parameters filled up. So if we pass Char as the type parameter to Maybe, we get a type of Maybe Char. The value Just 'a' has a type of Maybe Char, for example. Most of the time, we don’t pass types as parameters to type constructors explicitly. That’s because Haskell has type inference. So when we make a value Just 'a', for example, Haskell figures out that it’s a Maybe Char. If we want to explicitly pass a type as a type parameter, we must do it in the type part of Haskell, which is usually after the :: symbol. This can come in handy if, for example, we want a value of Just 3 to have the type Maybe Int. By default, Haskell will infer the type (Num a) => Maybe a for that value.

 

pages: 999 words: 194,942

Clojure Programming by Chas Emerick, Brian Carper, Christophe Grand

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

Amazon Web Services, Benoit Mandelbrot, cloud computing, continuous integration, database schema, domain-specific language, en.wikipedia.org, failed state, finite state, Firefox, game design, general-purpose programming language, mandelbrot fractal, Paul Graham, platform as a service, premature optimization, random walk, Schrödinger's Cat, semantic web, software as a service, sorting algorithm, Turing complete, type inference, web application

Preserving user-provided type hints Most macros discard the metadata attached to the forms within their context, including type hints.[182] For example, here the or macro form does not propagate the ^String type hint to the code it produces, resulting in a reflection warning: (set! *warn-on-reflection* true) ;= true (defn first-char-of-either [a b] (.substring ^String (or a b) 0 1)) ; Reflection warning, NO_SOURCE_PATH:2 - call to substring can't be resolved. ;= #'user/first-char-of-either Note Such cases are rarely found in the wild, because type hints are usually put upstream of interop calls, resulting in the type of the macro form being determined through type inference: (defn first-char-of-either [^String a ^String b] (.substring (or a b) 0 1)) ;= #'user/first-char-of-either We can verify that the hint metadata on the or expression is lost; here, the expression, with metadata: (binding [*print-meta* true] (prn '^String (or a b))) ; ^{:tag String, :line 1} (or a b) But if we macroexpand the same expression, that metadata is gone: (binding [*print-meta* true] (prn (macroexpand '^String (or a b)))) ; (let* [or__3548__auto__ a] ; (if or__3548__auto__ or__3548__auto__ (clojure.core/or b))) However, there’s no reason why the type hint on the or expression can’t be preserved; doing so simply requires using &form effectively in its macro definition.

.)) ;= #<ArrayList []> (accepts-anything 5) ;= 5 (accepts-anything false) ;= false This is in contrast to signature declarations, which Clojure does provide, but only for primitive arguments and return types. We cover primitive type declarations in Declare Functions to Take and Return Primitives. Avoiding reflective interop calls is key to ensuring maximal performance in code that is CPU-bound. In practice, little type-hinting is required in order to avoid reflection entirely, since the Clojure compiler provides for type inference based on the known types of literals, constructor calls, and method return types. To illustrate this, let’s add a type hint to some code in order to optimize it. Here’s a function that returns a provided String, capitalized: Example 9-12. An unhinted capitalization function (defn capitalize [s] (-> s (.charAt 0) Character/toUpperCase (str (.substring s 1)))) This implementation works, but we’d probably like to speed it up a little bit: Example 9-13.

. ;= #'user/capitalize We see here that three interop calls are being emitted reflectively. We can address this by adding a single type hint (notice the ^String addition): (defn fast-capitalize [^String s] (-> s (.charAt 0) Character/toUpperCase (str (.substring s 1)))) This will eliminate all three reflective calls. How can just one type hint impact all three reflective calls? This is where the Clojure compiler’s type inference comes into play: The let-bound name s is explicitly type-hinted to be a String. Therefore… …the .charAt call can be compiled down to a direct call to String.charAt. The compiler knows that this method returns a char, so… …it can properly select the char variant of Character.toUpperCase (rather than its int override). Finally, the compiler again refers back to the explicit String type hint on s to inform its selection of String.substring when compiling the .substring interop method call.

 

pages: 230

Purely Functional Data Structures by Chris Okasaki

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

reversible computing, Turing machine, type inference

His original data structure [Bro95] can be implemented purely functionally (and thus made persistent) by combining the recursive-slowdown technique of Kaplan and Tarjan [KT95] with a purely functional implementation of real-time deques, such as the real-time deques of Section 8.4.3. However, such an implementation would be both complicated and slow. Brodal and Okasaki simplify this implementation in [BO96], using skew binomial heaps (Section 9.3.2) and structural abstraction (Section 10.2.2). Polymorphic Recursion Several attempts have been made to extend Standard ML with polymorphic recursion, such as [Myc84, Hen93, KTU93]. One complication is that type inference is undecidable in the presence of polymorphic recursion [Hen93, KTU93], even though it is tractable in practice. Haskell sidesteps this problem by allowing polymorphic recursion whenever the programmer provides an explicit type signature. 11 Implicit Recursive Slowdown In Section 9.2.3, we saw how lazy redundant binary numbers support both increment and decrement functions in 0(1) amortized time.

Texts and Monographs in Computer Science. Springer-Verlag, New York, 1981. (p. 55) [GS78] Leo J. Guibas and Robert Sedgewick. A dichromatic framework for balanced trees. In IEEE Symposium on Foundations of Computer Science, pages 8-21, October 1978. (pp. 24,29, 99) [GT86] Hania Gajewska and Robert E. Tarjan. Deques with heap order. Information Processing Letters, 22(4): 197-200, April 1986. (p. 113) [Hen93] Fritz Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253-289, April 1993. (p. 170) [HJ94] Paul Hudak and Mark P. Jones. Haskell vs. Ada vs. C++ vs An experiment in software prototyping productivity, 1994. (p. 1) [HM76] Peter Henderson and James H. Morris, Jr. A lazy evaluator. In ACM Symposium on Principles of Programming Languages, pages 95-103, January 1976.

 

pages: 752 words: 131,533

Python for Data Analysis by Wes McKinney

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

backtesting, cognitive dissonance, crowdsourcing, Debian, Firefox, Google Chrome, index card, random walk, recommendation engine, revision control, sentiment analysis, Sharpe ratio, side project, sorting algorithm, statistical model, type inference

The options for these functions fall into a few categories: Indexing: can treat one or more columns as the returned DataFrame, and whether to get column names from the file, the user, or not at all. Type inference and data conversion: this includes the user-defined value conversions and custom list of missing value markers. Datetime parsing: includes combining capability, including combining date and time information spread over multiple columns into a single column in the result. Iterating: support for iterating over chunks of very large files. Unclean data issues: skipping rows or a footer, comments, or other minor things like numeric data with thousands separated by commas. Type inference is one of the more important features of these functions; that means you don’t have to specify which columns are numeric, integer, boolean, or string.

.: return x + y In [135]: add_them = np.frompyfunc(add_elements, 2, 1) In [136]: add_them(np.arange(8), np.arange(8)) Out[136]: array([0, 2, 4, 6, 8, 10, 12, 14], dtype=object) Functions created using frompyfunc always return arrays of Python objects which isn’t very convenient. Fortunately, there is an alternate, but slightly less featureful function numpy.vectorize that is a bit more intelligent about type inference: In [137]: add_them = np.vectorize(add_elements, otypes=[np.float64]) In [138]: add_them(np.arange(8), np.arange(8)) Out[138]: array([ 0., 2., 4., 6., 8., 10., 12., 14.]) These functions provide a way to create ufunc-like functions, but they are very slow because they require a Python function call to compute each element, which is a lot slower than NumPy’s C-based ufunc loops: In [139]: arr = randn(10000) In [140]: %timeit add_them(arr, arr) 100 loops, best of 3: 2.12 ms per loop In [141]: %timeit np.add(arr, arr) 100000 loops, best of 3: 11.6 us per loop There are a number of projects under way in the scientific Python community to make it easier to define new ufuncs whose performance is closer to that of the built-in ones.

 

pages: 194 words: 36,223

Smart and Gets Things Done: Joel Spolsky's Concise Guide to Finding the Best Technical Talent by Joel Spolsky

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

Build a better mousetrap, knowledge worker, linear programming, nuclear winter, Sand Hill Road, Silicon Valley, sorting algorithm, Superbowl ad, the scientific method, type inference, unpaid internship

And while everyone else their age was running around playing “soccer” (this is a game many kids who can’t program computers play that involves kicking a spherical object called a “ball” with their feet (I know, it sounds weird)), they were in their dad’s home office trying to get the Linux kernel to compile. Instead of chasing girls in the playground, they were getting into flamewars on Usenet about the utter depravity of programming languages that don’t implement Haskell-style type inference. Instead of starting a band in their garage, they were implementing a cool hack so that when their neighbor stole bandwidth over their openaccess Wi-Fi point, all the images on the web appeared upside-down. BWA HA HA HA HA! So, unlike, say, the fields of law or medicine, over here in software development, by the time these kids are in their second or third year in college, they are pretty darn good programmers.

 

pages: 496 words: 174,084

Masterminds of Programming: Conversations With the Creators of Major Programming Languages by Federico Biancuzzi, Shane Warden

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

business intelligence, business process, cellular automata, cloud computing, complexity theory, conceptual framework, continuous integration, data acquisition, domain-specific language, Douglas Hofstadter, Fellow of the Royal Society, finite state, Firefox, follow your passion, Frank Gehry, general-purpose programming language, HyperCard, information retrieval, iterative process, John von Neumann, linear programming, loose coupling, Mars Rover, millennium bug, NP-complete, Paul Graham, performance metric, QWERTY keyboard, RAND corporation, randomized controlled trial, Renaissance Technologies, Silicon Valley, slashdot, software as a service, software patent, sorting algorithm, Steve Jobs, traveling salesman, Turing complete, type inference, Valgrind, Von Neumann architecture, web application

The hallmark of a good language feature is that you can use it in more than just one way. Again, I’ll use LINQ as an example here. If you break down the work we did with LINQ, it’s actually about six or seven language features like extension methods and lambdas and type inference and so forth. You can then put them together and create a new kind of API. In particular, you can create these query engines implemented as APIs if you will, but the language features themselves are quite useful for all sorts of other things. People are using extension methods for all sorts of other interesting stuff. Local variable type inference is a very nice feature to have, and so forth. We could’ve probably shipped something like LINQ much quicker if we said, “Let’s just jam SQL in there or something that is totally SQL Server-specific, and we’ll just talk to a database and then we’ll have it,” but it’s not general enough to merit existence in a general-purpose programming language.

“The Essence of XML,” Preliminary version: POPL 2003, New Orleans (January 2003). Chapter 9. ML ML is a general-purpose functional language developed by Robin Milner and the team he led at the University of Edinburgh in the 1970s. It grew from a metalanguage project designed to describe mathematical proofs. ML’s most valuable contribution to language design may be the Hindley-Milner type inference algorithm used in many static, latent type systems. The language inspired Standard ML, Caml, Haskell, and F#, among others. The Soundness of Theorems You created LCF, one of the first tools for automated theorem proving, and the programming language ML to run the proving. How did it work? Robin Milner: There were other efforts at machine-assisted proof around in 1970. They were at two extremes: either fully inventive (e.g., using Robinson’s famous resolution principle) in searching for a proof, or fully noninventive in the sense that they would only check that each small step performed by a human was logically valid (as in de Bruijn’s Automath system).

 

pages: 536 words: 73,482

Programming Clojure by Stuart Halloway, Aaron Bedra

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

continuous integration, en.wikipedia.org, general-purpose programming language, Gödel, Escher, Bach, Paul Graham, type inference, web application

When benchmarking, you’ll tend to want to take several measurements so that you can eliminate start-up overhead plus any outliers; therefore, you can call time from inside a dotimes macro: ​(dotimes bindings & body)​ dotimes will execute its body repeatedly, with the name bound to integers from zero to n-1. Using dotimes, you can collect five timings of sum-to as follows: ​(dotimes [_ 5] (time (sum-to 10000)))​ ​| "Elapsed time: 0.149 msecs"​ ​| "Elapsed time: 0.126 msecs"​ ​| "Elapsed time: 0.194 msecs"​ ​| "Elapsed time: 0.279 msecs"​ ​-> "Elapsed time: 0.212 msecs"​ To speed things up, you can hint the argument and return type as long. Clojure’s type inference will flow this hint to all the internal operations and function calls inside the function. ​(defn ^long integer-sum-to [^long n]​ ​ (loop [i 1 sum 0]​ ​ (if (< = i n)​ ​ (recur (inc i) (+ i sum))​ ​ sum)))​ The integer-sum-to is indeed faster: ​(dotimes [_ 5] (time (integer-sum-to 10000)))​ ​| "Elapsed time: 0.044 msecs"​ ​| "Elapsed time: 0.023 msecs"​ ​| "Elapsed time: 0.025 msecs"​ ​| "Elapsed time: 0.023 msecs"​ ​-> "Elapsed time: 0.02 msecs"​ Clojure’s primitive math is still correct, in that it will check for overflow and throw an exception.

 

pages: 224 words: 48,804

The Productive Programmer by Neal Ford

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

anti-pattern, business process, c2.com, continuous integration, database schema, domain-specific language, Firefox, general-purpose programming language, knowledge worker, side project, type inference, web application, William of Occam

The productivity comes from working close to the problem domain in the DSL; the power comes from the abstraction layer simmering just below the surface. Expressive DSLs on top of powerful languages will become the new standard. Frameworks will be written using DSLs, not on top of statically typed languages with restrictive syntax and unnecessary ceremony. Note that this isn’t necessarily a dynamic language or even a Ruby tirade: a strong potential exists for statically typed type-inference languages that have a suitable syntax to also take advantage of this style of programming. For an example of this, check out Jaskell* and, in particular, the build DSL written on top of it called Neptune.† Neptune performs the same basic tasks as Ant, but it is written as a domain-specific language atop Jaskell. It shows how readable and concise you can make code in Jaskell, using a familiar problem domain.

 

pages: 292 words: 81,699

More Joel on Software by Joel Spolsky

Amazon: amazon.comamazon.co.ukamazon.deamazon.fr

barriers to entry, Black Swan, Build a better mousetrap, business process, call centre, Danny Hillis, failed state, Firefox, George Gilder, low cost carrier, Mars Rover, Network effects, Paul Graham, performance metric, place-making, price discrimination, prisoner's dilemma, Ray Oldenburg, Sand Hill Road, Silicon Valley, slashdot, social software, Steve Ballmer, Steve Jobs, Superbowl ad, The Great Good Place, type inference, unpaid internship, wage slave, web application, Y Combinator

And while everyone else their age was running around playing soccer (this is a game many kids who can’t program computers play that involves kicking a spherical object called a ball with their feet—I know, it sounds weird), they were in their dad’s home office trying to get the Linux kernel to compile. Instead of chasing girls in the playground, they were getting into flamewars on Usenet about the utter depravity of programming languages that don’t implement Haskell-style type inference. Instead of starting a band in their garage, they were implementing a cool hack so that when their neighbor stole bandwidth over their open-access Wi-Fi point, all the images on the Web appeared upside-down. BWA HA HA HA HA! So, unlike, say, the fields of law or medicine, over here in software development, by the time these kids are in their second or third year in college they are pretty darn good programmers.