[
index : Fin n -> Vect n a -> a
index n v = unsafeGetIndex ( FS (FS (coerence n))) v
index n v = unsafeGetIndex ( FS (FS (coerence n))) v
Size: a a a
2021 May 31
[
Конечный сет
gо
Тебе не положено думать про рантайм
AN
gо
Idris игрушечный, так что оптимизировали ли они хотя бы Nat в рантайме — хз
[
У него в доке на первой страничке написано
AN
В хаскеле было бы struct Nat { Nat* succ }
[
Настолько всех этот вопрос волнует
[
Я не уверен если что
AN
Я тоже
[
Например, те же листы хаскель умеет своить до массивов, а иногда даже до генераторов
[
И какая-то хуйня типа
[1..] получается O(1) по памятиr
Nat оптимизируется. Унарное представление чисел это слишком тормозно даже для игрушечных примеров.
gо
Или ещё до чего-нибудь
Тебе не положено думать о рантайме
Тебе не положено думать о рантайме
gо
Ну хоть так
Но интересно, захардкожен Nat или они придумали, как эту оптимизацию генерализовать
Но интересно, захардкожен Nat или они придумали, как эту оптимизацию генерализовать
[
Мы вчера тоже до этого вопроса дошли
AN
Значит если я сгенерировал Nat а потом пытаюсь сматчить его на S k, то он просто в рантайме сравнивает число с нулем.
[
Если захардкочен, то мой Fin - хуйня жуткая
[
Если нет, то норм тема
AN
Так а зачем вообще значение n из Fin n в рантайме.