Różnica między typami i rodzajami

To może być bardzo proste pytanie.

Ale jaka jest różnica między rodzajami i rodzajami?

Moje obecne rozumienie jest takie, że masz teorię typów z regułami typów, które dają pojęcie dobrze napisanego wyrażenia, ale rodzaje są bardziej podstawowe, różnicując symbole na różne rodzaje symboli i wprowadzając podstawowe zasady dotyczące stosowania funkcji itp.

Być może jest niewielka różnica, może po prostu pochodzą z różnych dziedzin. Ale nie mogę znaleźć jasnego opisu ich relacji.

Rozumiem różnicę w tym, że te dwie koncepcje służą do nieco odmiennego podkreślenia, ale ostatecznie są one w pewnym sensie tym samym. Ponieważ żadna z nich nie ma formalnej definicji, nie możemy oczekiwać dokładnej odpowiedzi bez uprzedniego ograniczenia zakresu do szczególnego zrozumienia „typu” i „sortowania”.

„Sortowanie” jest używane, gdy chcemy powiedzieć, że istnieje kilka różnych, no cóż, rodzajów rzeczy, które musimy rozróżnić. Przykładem może być teoria geometrii z sortowaniem „punkt” i „linia”.

„Typ” jest używany, gdy nie tylko istnieje potrzeba rozróżnienia różnych rodzajów rzeczy, ale należyta uwaga jest poświęcona strukturze samych rodzajów / typów. Tak więc zazwyczaj możemy tworzyć nowe typy ze starych (produkty, sumy, typy funkcji), możemy mieć ciekawe relacje między typami (równość typów, podtypy) itp. W przeciwieństwie do tego, zazwyczaj na początku określa się niektóre rodzaje, a wtedy nigdy nie przywiązuje dużej wagi do struktury klasy wszelkiego rodzaju.

Tak przynajmniej postrzegam różnicę, inni ludzie mogą mieć różne doświadczenia.

Jak mówi Andrej, żaden termin nie jest całkowicie formalny i mówi o mniej więcej takich samych rzeczach, więc tak naprawdę nie ma wyraźnej linii podziału.

$t$$\sigma$$t : \sigma$$[\![t]\!] \in [\![\sigma]\!]$

$e$$\tau$$e : \tau$