История изменений

Скажу как человек знакомый со скалой (правда уже и забывший, по большому счёту) и с хаскелем: могу сказать что зависимые типы там конечно есть и даже бывают(в скале) применяются, емнип. Но вот в хаскеле они «есть», но как например там реализовать filter? в идрисе есть **. Это (хаскель/скаль)-ное «есть» - это не совсем «есть», это просто максимум что смогло предыдущее поколение языков. По моему, это скорее «ну почти дотянули», чем «есть». Пользоваться этим в хаскеле я так понял на практике широко невозможно (я пытался раз, месяца два назад, из любопытства). В скале я не пытался пользоваться, но думаю что ситуация хуже чем в хаскеле.

Как там в F* я не знаю, но если где-то так же как в хаскеле, то это банально неудобно.

Идрис/агда - совсем другой уровень. Там зависимые типы действительно можно попробовать использовать широко на практике: кажется, для этого всё готово.

Скажу как человек знакомый со скалой (правда уже и забывший, по большому счёту) и с хаскелем: могу сказать что зависимые типы там конечно есть и даже бывают(в скале) применяются, емнип. Но вот в хаскеле они «есть», но как например там реализовать filter? в идрисе есть **. Это (хаскель/скаль)-ное «есть» - это не совсем «есть», это просто максимум что смогло предыдущее поколение языков. По моему, это скорее «ну почти дотянули», чем «есть». Пользоваться этим в хаскеле я так понял на практике широко невозможно (я пытался раз из любопытства). В скале я не пытался пользоваться, но думаю что ситуация хуже чем в хаскеле.

Как там в F* я не знаю, но если где-то так же как в хаскеле, то это банально неудобно.

Идрис/агда - совсем другой уровень. Там зависимые типы действительно можно попробовать использовать широко на практике: кажется, для этого всё готово.

Скажу как человек знакомый со скалой (правда уже и забывший, по большому счёту) и с хаскелем: могу сказать что зависимые типы там конечно есть и даже бывают(в скале) применяются, емнип. Но вот в хаскеле они «есть», но как например там реализовать filter? в идрисе есть **. Это (хаскель/скаль)-ное «есть» - это не совсем «есть», это просто максимум что смогло предыдущее поколение языков. По моему, это скорее «ну почти дотянули», чем «есть». Пользоваться этим в хаскеле я так понял на практике широко невозможно (я пытался раз из любопытства). В скале я не пытался пользоваться, но думаю что ситуация хуже чем в хаскеле.

Как там в F* я не знаю, но если где-то так же как в скала/хаскеле, то это банально неудобно.

Идрис/агда - совсем другой уровень. Там зависимые типы действительно можно попробовать использовать широко на практике: кажется, для этого всё готово.

Скажу как человек знакомый со скалой (правда уже и забывший, по большому счёту) и с хаскелем: могу сказать что зависимые типы там конечно есть и даже бывают(в скале) применяются, емнип. Но вот в хаскеле они «есть», но как например там реализовать filter? в идрисе есть **. Это (хаскель/скаль)-ное «есть» - это не совсем «есть», это просто максимум что смогло предыдущее поколение языков. По моему, это скорее «ну почти дотянули», чем «есть». Пользоваться этим в хаскеле я так понял на практике широко невозможно (я пытался раз из любопытства). В скале я не пытался пользоваться, но думаю что ситуация хуже чем в хаскеле.

Идрис/агда - совсем другой уровень. Там зависимые типы действительно можно попробовать использовать широко на практике: кажется, для этого всё готово.

Скажу как человек знакомый со скалой (правда уже и забывший, по большому счёту) и с хаскелем: могу сказать что они там конечно есть и даже бывают(в скале) применяются, емнип. Вот в хаскеле они «есть», но вот как например там реализовать filter? в идрисе есть **. Это (хаскель/скаль)-ное «есть» - это не совсем «есть», это просто максимум что смогло предыдущее поколение языков. По моему, это скорее «ну почти дотянули», чем «есть». Пользоваться этим в хаскеле я так понял на практике широко невозможно (я пытался раз из любопытства). В скале я не пытался пользоваться, но думаю что ситуация хуже чем в хаскеле.

Идрис/агда - совсем другой уровень. Там зависимые типы действительно можно попробовать использовать широко на практике: кажется, для этого всё готово.

Скажу как человек знакомый со скалой (правда уже и забывший, по большому счёту) и с хаскелем: могу сказать что они там конечно есть и даже бывают(в скале) применяются, емнип. Вот в хаскеле они «есть», но вот как например там реализовать filter? в идрисе есть **. Это (хаскель/скаль)-ное «есть» - это не совсем «есть», это просто максимум что смогло предыдущее поколение языков. По моему, это скорее «ну почти дотянули», чем «есть». Пользоваться этим в хаскеле я так понял на практике широко невозможно (я пытался раз из любопытства). В скале я не пытался пользоваться, но думаю что ситуация хуже чем в хаскеле.

Идрис/агда - совсем другой уровень. Там зависимые типы действительно можно попробовать использовать широко на практике. Кажется, для этого всё готово.

Скажу как человек знакомый со скалой (правда уже и забывший, по большому счёту) и с хаскелем: могу сказать что они там конечно есть и даже бывают(в скале) применяются, емнип. Вот в хаскеле они «есть», но вот как например там реализовать filter? в идрисе есть **. Это (хаскель/скаль)-ное «есть» - это не совсем «есть», это просто максимум что могло выжать предыдущее поколение языков. По моему, это скорее «ну почти дотянули», чем «есть». Пользоваться этим в хаскеле я так понял на практике широко невозможно (я пытался раз из любопытства). В скале я не пытался пользоваться, но думаю что ситуация хуже чем в хаскеле.

Идрис/агда - совсем другой уровень. Там зависимые типы действительно можно попробовать использовать широко на практике. Кажется, для этого всё готово.