Здравствуйте, DarkGray, Вы писали:
DG>сорт и kind — это одно и тоже?
Нет, довольно таки разные вещи.
>> на типах вы можете сделать всё что угодно, при условии что этого никак нельзя будет наблюдать в окружающем мире
DG>а почему нельзя использовать функцию, которая распакует сорт в реальное значение?
Не уверен, что правильно понял вопрос, если отвечу невпопад, то уточни вопрос.
В ряде случаев это тавтология, например значение типа int 3 может быть только тройкой, статика и динамика совпадают, распаковывать ничего не нужно. А в ряде других случаев мы упираемся в то, что статические значения используются только в компайл-тайме, в рантайме их просто нет. Банальный пример — тип list(int, 10) (т.е. список из 10 интов) в рантайме представлен классическим односвязным списком, длина нигде не хранится. Просто при компиляции компилятор проверит все равенства и неравенства, упоминающие длину этого списка, на непротиворечивость и, если все ок, выдаст корректный код, в котором не будет например обращений к 11-му элементу данного списка. Но чтобы получить в рантайме длину этого списка как рантайм-значение, его надо честно вычислить, обойдя список.