W dniu wtorek, 20 listopada 2018 14:38:53 UTC+1 użytkownik Maciej Sobczak napisał:
> > Warto przyjrzeć się językowi Idris i typom zależnym.
>
> Nie przekonują mnie. Jeśli je rozumiem, to typy zależne pozwalają związać warunki
między parametrami i wartością zwracaną z funkcji. Fajnie, ale to nie wyczerpuje
tematu, bo jest jeszcze stan (również globalny), który też mogę chcieć związać takimi
warunkami.

Nie wiem, czy to wyczerpuje temat, ale na pewno jest
przykładem czegoś, co zwiększa ilość rzeczy, które możemy
statycznie powiedzieć o naszym programie.

Tutaj jest prezentacja o tym, w jaki sposób typy zależne
umożliwiają wyrażanie błędów w programach (na przykładzie
Heartbleed, przy użyciu Liquid Haskell):
https://www.youtube.com/watch?v=YByOdE-YUwY

> Co więcej, takie warunki nie muszą mieć związku z typami - np. jedna metoda w
obiekcie może "obiecać" inne warunki końcowe, niż inna metoda, a przecież nie jest
tak, że typ obiektu jest różny w różnych metodach. Takie ograniczenie już na poziomie
terminologii wskazuje, że typy zależne to domena jakiejś niszy językowej (w
szczególności języków funkcjonalnych), więc od razu ma dla mnie ograniczoną
stosowalność.

Ja nie jestem co do tego przekonany. Tzn. mnie się to też
nie wydaje naturalne, ale często "naturalność" to po prostu
kwestia przyzwyczajenia.

> Potrzebny jest inny formalizm. Pre- i post-conditions wydają się być bardziej
niekonfliktowym mechanizmem, tzn. możliwym do zastosowania bez niepotrzebnych
ograniczeń.

Jest też język ATS (trochę protoplasta Rusta), który
ma system "typów liniowych" służących do wyrażania twierdzeń
o poprawności korzystania z zasobów. Ale wydaje się raczej
trudny do używania:
https://www.youtube.com/watch?v=zt0OQb1DBko