Názory k článku Definice uživatelských datových typů v jazyku OCaml

Od GADT je už jen krůček k závislostním typům :) Tak co to bude, Agda, Coq, Lean nebo Idris?

K tomu musím ještě dorůst :-) ale asi Idris.

Jo, ten je asi nejlepší na učení. V praxi pak Lean (ten je taky víc ML-like).

> Popíšeme si, jakým způsobem lze uživatelské datové typy definovat v programovacím jazyku OCaml. Uvidíme, že mezi oběma jazyky existují v této oblasti rozdíly,

Které oba jazyky? Vidím tu jen zmínku o OCaml. Který je ten druhý? Nejspíš se tu něco ztratilo při editaci.

Jde o F#.

v redakci mi zkracuji perexy. Zrovna tady se to zkratilo tak, ze to nedava smysl, ale puvodne tam bylo:

Na článek o definicích uživatelských datových typů v jazyku F# dnes navážeme, protože si řekneme, jakým způsobem lze uživatelské datové typy definovat v programovacím jazyku OCaml. Uvidíme, že mezi oběma jazyky existují v této oblasti rozdíly, většinou však jen syntaktické.

Díky, tušil jsem, že za tím bylo něco podobného.