Jeg forstår ikke, hvorfor du mener, at F#, Haskell og O'Caml ikke har statiske typer, det har de i allerhøjeste grad.

Men det var måske på grund af, at de ikke kører på JVM, at du fravalgte dem? Der findes en variant af Haskell, kaldet Frege, som kører på JVM. Der findes også en JVM implementering af Standard ML på JVM, men den har ikke været opdateret i mange år, og OCaml-Java er stadig i alpha-version, så vidt jeg kan se. Så Frege er nok indtil videre det mest oplagte valg udover Scala til statisk typet funktionsprogrammering på JVM.

Og Scala er efter min mening ikke specielt kønt. F.eks. har notationen for algebraiske datatyper (case classes i Scala) meget boilerplate, og manglen på global typeinferens medfører også meget boilerplate.

Med de første erfaringer med Ceylon. Lyder ret interessant!

NB: Der findes mulighed for statiske typer i Clojure, men jeg kan sagtens forstå du vælger Clojure fra, da det desværre blev lidt af en syntax rodebutik.

Men har du overvejet FreePascal?

Jeg er godt klar over at "nogen" mener det er gammeldags, men brugerskaren er altså ikke slet så lille som nogen vil italesætte den til, og væsentlig større end de fleste af de andre småsprog du nævner.

Og lige præcis typing er en af de ting jeg rigtig godt kan lide ved Pascal (plus det at man imo har et rigtig godt overblik over hvad det egentlig er man laver).

Kan det køre på JVM?

http://wiki.freepascal.org/FPC_JVM

Men jeg har ingen erfaring med hvor godt eller dårligt det virker, da JVM ikke er noget issue for mig.

Det er det til gengæld for bloggere, og det er også årsagen til at der ikke er så mange der er bidt på det her blogindlæg. Det er altid spændende at snakke programmeringssprog, men ikke hvis man lader diskussionen begrænse af implementeringsteknologi. Ville man ikke synes jeg var fjollet, hvis jeg kun ville bruge sprog hvis oversættere var bygget med LLVM? Kravet om at et sprog skal kunne køre (godt) på JVM sætter en masse grænser for sprogdesignerens kreativitet, og det medfører uværgeligt mere kedelige sprog.

Derudover, i nutidens verden med mikrotjenester og decentraliseret arkitektur, er det så ikke nemmere end nogensinde før at have systemer der er skrevet i forskellige sprog?

Lidt on-topic: Jeg er stor tilhænger af Ceylon's syntaksfascisme. En af de få ting et sprog som Go gør meget rigtigt er at aflive cykelskursargumenter om formatering og deslige. Ved at kræve at syntaktisk forskellige elementer (f.eks. værdikonstruktører og variabelnavne) er leksikalt forskellige, f.eks. ved at førstnævnte skal starte med stort bogstav, kan man også tillade en letvægts-syntaks der stadigvæk er entydig. Det er en af grundene til at jeg synes Haskells syntaks for mønstergenkendelse er meget pænere end SMLs ditto.

Er påstanden ikke at det er umuligt at kombinere global type inferens og objekt orienteret programmering, i hvert fald den type som Scala implementere?

Helt annoteringsfri global typeinferens er uafgørlig, hvis der er subtyping (nedarvning), ja, men det kan lade sig gøre, hvis man enten fravælger dynamisk nedarvning (det ville være mit valg, man kan komme ret langt med statisk nedarvning) eller gør nedarvning eksplicit. Generelt vil jeg undgå features, der gør global typeinferens (i praksis) umulig. Der findes sprog, der i praksis fungerer fint med uafgørlige typesystemer, fordi de instanser, der er uafgørlige, forekommer meget sjældent.

Helt generelt synes jeg, at dynamisk nedarvning er oversolgt: De fleste af de fordele, det giver, fås lige så godt eller bedre med parametrisk polymorfi og statisk nedarvning, og i praksis medfører dynamisk nedarvning en del køretidscheck, da f.eks. A[] logisk set ikke er en subtype af B[], selv om A er en subtype af B. Derfor skal man enten lave et køretids typecheck når man indsætter værdier i et array (Javas løsning) eller tager værdier ud af et array (C#s løsning). Nedarvning i kombination med parametrisk polymorfi har et lignende problem.

Stort set det eneste sted, hvor dynamisk nedarvning giver en fordel, er heterogene samlinger, altså f.eks. lister, hvor elementerne har forskellige typer. Det kan dog klares med enten sumtyper eller eksistentielle typer i stedet.

Jeg antager dit fravlag Clojure skyldes en formodning om at det ikke understøtter navigering. Jeg er indrømmet ikke den store Clojure men de af Clojures fætre jeg kender (Common Lisp, Emacs Lisp) har ikke nogen problemer med at vide præcis hvor en funktion er defineret eller hvilke argumenter en funktion tager. Da den slags har været given funktionalitet siden Lisp maskinerne kom frem i 70'erne skulle det under mig meget om ikke Clojure understøtter dette også.

Source introspection er altså ikke noget der er snævert knyttet til statiske typer. Er det noget du har undersøgt (mht Clojure) eller hoppede du direkte til konklusionen?

Fair nok, men det er så heller ikke helt den samme problemstilling som det at vide hvor ting er defineret henne, som var noget af det der blev fremhævet.

Det er nok bare mig der er gammeldags, men jeg har lidt svært ved at se at automatiseret refaktorering kan gøre noget værdifuldt for en stor applikation.

Det modsiger jeg ikke, men at vide hvor noget er defineret kræver ikke statiske typer. Har du en rimeligt moderne Emacs i nærheden, kan du nemt prøve det selv.

Jeg kender for lidt til automatisk refaktorering til at kunne vurdere i hvor høj grad statiske typer er nødvendige i forhold til at lave rene source-til-source ændringer eller "blot" at have haskell-niveau type-inferens.

Man skal ihverfald ikke blande det sammen med at visse sprog har så kludret en syntaks at bare det for et værktøj at parse det, nærmest synes uafgørligt. Det løser til eksempel Lisp ved at have en meget enkel og stringent syntaks som nemt lader sig læse ind og behandle.

Har du nogen eksempler på typer af refaktoreringer hvor statisk typning er en forudsætning?

Jeg vil hævde at statiske typer også er en kæmpe hjælp ved manuelle refaktoreringer. Hvordan ved du ellers at du ikke har lavet fejl? Det er nemt at overse noget, men så er det heldigt hvis oversætteren kan sætte en bremse i.

Jeg vil lige indskyde at Haskell-niveau type-inferens faktisk er et endnu stærkere værktøj end Javas relativt typesystem, også selvom man ikke selv skal angive typer for hver variabelbinding. Blot fordi man skal skrive en masse boilerplate er typesystemet ikke nødvendigvis stærkt, eller nemmere at behandle for værktøjer.

Nogle omskrivninger forudsætter, at værdier er immutable (ikke kan modificeres efter initialisering), og det fremgår af typen i f.eks. SML. Andre omskrivninger forudsætter, at lighed er defineret for typen, hvilket også fremgår af typen.

Det er jo her det lidt, for mig, begynde at ligne en selvskabt plage. Har man et dynamisk typet sprog har man jo netop ikke behov for at gå rundt og opdatere alle instanser.

Det er jo lidt det der er humlen, med rigtige statiske typer (som i Java), betaler man en pris for hver eneste sted (variabel/attribut/parameter), hver gang, hele tiden. Med dynamisk typning kan man lægge type-annoteringer på efter behov. Og selv med dynamisk typning er det jo ikke sådan at compileren bare giver op og helt lader være med at checke noget som helst.

Det er ikke fordi dit eksempel er forkert, ligesom det heller ikke er forkert at statisk typning vil forhindre visse klasser af fejl, problemet er bare om det i praksis betyder nok til at man genindvinder den pris man har betalt up front.

Det er selvfølgeligt klart at hvis man et 500.000 liniers program med tusindvis af klasser og masser af overloadede 4 bogstavs metode navne, så har man da brug for hjælp .... af værktøjet :-)

Givet, men det er vel ikke et ret godt eksempel for en Java programmør?

Som Mikkel sagde, så er det kun simple ændringer såsom skift af typen af en enkelt parameter, hvor dynamiske typer gør det unødvendigt at omskriv en masse erklæringer. Lige præcis den samme fordel giver glibal typeinferens: Du skal ikke skrive typen af parametre, så hvis du laver en parameter om fra f.eks. heltal til bool, så skal du ikke omskrive erklæringer. Typeinferensen vil endvidere fortælle dig præcis, hvor det er nødvendigt at lave omskrivninger, f.eks. ved brug af konstanter.

Næsten alle de fordele, som dynamiske typer giver, får man også med global typeinferens. Igen er den eneste praktisk relevante undtagelse heterogene collections, hvor man skal bruge en sumtype (datatype), hvis man vil have fuld statisk typesikkerhed og global typeinferens. Eksistentielle typer kan også gøre det, men det kræver eksplicit typeannotering.

Med et statisk type system er der en omkostning up-front i og med der skal skrives erklæringer på alle places og de skal vedligeholdes. Ændrer en type sig (eg nyt navn) er ikke bare noget kode muligvis berørt, men alle steder det gamle typenavn er skrevet ind, skal også opdateres. Med dynamiske typer eller statisk type inferens, der er ikke noget af den slags adminstration.

Det er ikke det samme som at der er en netto omkostning. Det er muligt (og mange er åbentlyst af den mening) at man får så mange tidsbesparelser længere henne i forløbet (som f.eks. tool assisted refaktorering eller forhindring af visse fejl) at det mere end opvejer den ekstra administration. Men der er en ekstra administration (rent source kode mæssigt) ved statiske typer som ikke findes i alternativerne.