No vidíš, to je přesně ono, ověřování invariantů. Rozdíl je jen v tom, že v jazycích jako Idris či Lean (nebo SPARK, ale tam se používá jiná metoda) překladač provede verifikace při překladu (nemusí se dělat runtime check), i když velikost není konstantní. (Už to asi nechceme hlouběji rozebírat, ale umožňují to sigma typy. Jinak jo, v Rustu se dá s generickými parametry taky dělat psí kusy a časem třeba přidají i něco à la Lean, nejen typy, ale i plnohodnotnou funkcionální sémantiku
Tak počítám, že tohle by se dalo udělat i s dynamickým polem, ono je celkem jedno, jak ten invariant vyrobim. Ale nezkoušel jsem si to zatim. Jo, vim co jsou dependent types. U Rustu postup směrem k něčemu takovému nebo k HKTs moc nečekej, přeci jen, je to jazyk určený pro reálný, praktický engineering, ne pro postgraduální bádání apod. Když už, tak se spíš teď mudruje nad efekty, resp. specificky control-flow efekty, kvůli error handlingu, generátorům, async streamům apod. Opět ale nečekej nějaký těžce obecný systém, pravděpodobně by to přinejlepším byl opět nějaký subset, se zaměřením na zero-costness, ergnomii a nepříliš strmou učící křivku spíš než krásy typových systémů.
Swift už ji nějakou dobu má, takže je ověřené, že to jde i v tomto typu jazyků.
Jakou featuru Swiftu máš na mysli? Jinak Swift není stejný typ jazyka, nezaměřuje se na zero-cost abstrakce, má runtime, OOP s implicitním dynamic dispatchem,...
P.S. BTW zajímalo by mne, zda by šlo v Rustu nějak zprovoznit toto: https://ericniebler.com/2013/07/16/f-algebras-and-c/ ![Úsměv :)](http://forum.root.cz/Smileys/default/smiley.gif)
Čistě typovým systémem by to drhlo, v Rustu neuděláš ekvivalent
template<template<typename> class F>
struct Fix, takže by se musela třeba napsat nějaká traita a tu pak implementovat pro typy, které bys chtěl fixovat. S makrama by to mělo být bez problému. Ono koneckonců v tom C++ je to trochu švindl, protože ty templaty jsou duck typing, žejo...