В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

Haskell

1647 membersпожаловаться на группу
2021 January 09

к

кана in Haskell
эта эргономика потом вылелась в неопределенности в других пропосалах, где стало не ясно, @a патттерн это должен быть матчинг типа, или просто вайлдкард который перебинжевает переменную
источник
18:06пожаловаться#1

MP

Misha Puzanov in Haskell
ну тут у меня знаний не хватает, чтобы чего-то по делу сказать
источник
18:07пожаловаться#2

MP

Misha Puzanov in Haskell
однако в целом это вся тема дико не интуитивная
источник
18:08пожаловаться#3

к

кана in Haskell
Maxim Koltsov
Ты это ещё у агды спроси или у кока
так что ты хотел сказать-то этим, я не очень понял посыл
источник
18:08пожаловаться#4

MK

Maxim Koltsov in Haskell
кана
так что ты хотел сказать-то этим, я не очень понял посыл
Там же тоже есть значащие имена в сигнатурах
Или их нельзя использовать в теле определения?..
источник
18:11пожаловаться#5

к

кана in Haskell
конечно нельзя, они забинжены в типе сигнатуры, там и сидят
источник
18:12пожаловаться#6

к

кана in Haskell
так можно

Definition f : forall a, a -> Type :=
 fun a _ => a.


так нельзя, "a" забинжен в типе и никуда не вылезает

Definition f : forall a, a -> Type :=
 fun _ _ => a.
источник
18:13пожаловаться#7

к

кана in Haskell
в хаскеле же переменные из терма типа вылезают из терма в определение
источник
18:14пожаловаться#8

MK

Maxim Koltsov in Haskell
Спасибо
источник
18:14пожаловаться#9

MK

Maxim Koltsov in Haskell
Тупанул
источник
18:14пожаловаться#10

к

кана in Haskell
можно вот так

Definition f {a} (x : a) : Type := a.

это аналог нашего

f @a (x :: a) :: Type = a

если бы так можно было бы написать сейчас
источник
18:16пожаловаться#11

MK

Maxim Koltsov in Haskell
кана
можно вот так

Definition f {a} (x : a) : Type := a.

это аналог нашего

f @a (x :: a) :: Type = a

если бы так можно было бы написать сейчас
Фу блин, ужасно
источник
18:19пожаловаться#12

MK

Maxim Koltsov in Haskell
Короче я люблю форолы
источник
18:19пожаловаться#13

MK

Maxim Koltsov in Haskell
Везде
источник
18:19пожаловаться#14

к

кана in Haskell
ну за агду я не ручаюсь конечно, в новом идрисе уже тоже как в хаскеле

f : {a : Type} -> (x : a) -> Type
f _ = a
источник
18:19пожаловаться#15

к

кана in Haskell
f : {a : Type} -> (x : a) -> Type
f {a = b} _ = -- тут нет "a" в скоупе

но при этом если явно сбиндить, то переменная пропадает из скоупа
источник
18:22пожаловаться#16

MK

Maxim Koltsov in Haskell
Я за агду тоже
источник
18:25пожаловаться#17

MK

Maxim Koltsov in Haskell
Только на коке писал
источник
18:25пожаловаться#18

MK

Maxim Koltsov in Haskell
Агда мне вообще разонравилась заочно
источник
18:26пожаловаться#19

A

Andrey in Haskell
блин, выходит не удастся просто так обойти это ограничение между разницей в версиях Cabal и cabal-install
источник
19:04пожаловаться#20