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.

Statiske sprog har en langt mindre risiko for fejl hen ad vejen, da man opfanger typiske fejl allerede ved kompilering, før man overhovedet når at prøve det af. Og med en ordenlig IDE, allerede før det. Dynamiske sprog, udover at være sjovere at arbejde med, har en tendens til at gemme på små irriterende fejl, der rammes på sjældne tilfældige tidspunkter, som er næsten umulige at finde frem til, typisk fordi der sniger sig en forkert type ind et sted, hvor den ikke høre til. Hvis man ikke arbejder med voldsomt store projekter, så er de udmærkede, men et projekt kan godt komme op i en størrelse, hvor et statisk sprog vil være at fortrække. Tag Facebook som eksempel. De har forsøgt sig med Hack (fail), fordi PHP's tidligere mangel på ordenlige statiske egenskaber (før PHP7), voldte for mange problemer, når for mange folk, skulle arbejde på kryds af hinanden.

Du snakker om problemer, hvis navnet på en type ændre sig? Hvorfor gør den det? Et sprogs typer har jeg endnu ikke oplevet, at de blev omdøbt. Og egne typer? Hvorfor skulle man dog omdøbe sine ting? Hvis et navn ændre sig, så vil det som regel være fordi man laver større ændringer, struktur omlægning osv., hvorefter man alligevel vil skulle ændre de steder hvor det anvendes, hvilket er langt nemmere at finde frem til ved statiske sprog, og sikre at man har fået det hele med. Derudover hvis man har en ordenlig IDE, så vil den automatisk ændre navn alle steder hvor de er anvendt, hvis du omdøber noget. Med de mange fordele ved statiske sprog, og den meget lille sandsynlighed for at man lige ønsker et andet navn til sin class or whatnot, hvilket ens IDE bør kunne håndtere, så vil jeg nu mene at statiske sprog i det lange løb, spare langt flere penge, end hvad et dynamisk kan hente hjem.

Dertil skal det lige siges, at jeg er ikke fortaler for statiske sprog. Har ikke noget fordrukkent og anvender de sprog jeg synes passer bedst til/er tilgængelige til en given opgave, heriblandt dynamiske. Men at påstå at dynamiske sprog ligefrem skulle være besparende, den kan desværre ikke være med på.