ща, я мог что-то напутать, найду табличку

да, напутал, @ как бы делает невидимый аргумент видимым, то есть forall x. y тут x невидимый

а {} говорит, что этот аргумент нельзя сделать видимым, он может только вывестись

прикольно будет, если @ можно будет реализовать в виде оператора в будущем при желании, типа

(@) :: (forall (a :: k). b a) -> (forall (a :: k) -> b a)
f @ a = f :: b a

в лине

def {u} vis {A} {B : A -> Sort u} : (Π{x : A}, B x) → Π(x : A), B x :=
 λf x, (f : B x)

infixr @@:1 := vis

Всем привет!
Кто-нибудь помнит как называется тулза, чтобы визуализировать хаскельный проект в виде дерева из функций?

про нотацию с {} в первый раз слышу, спасибо

раз уж речь зашла про тайп аппликейшнс:

эмпирическими наблюдениями я понял, что порядок применения соответствует с порядком следования типовых переменных после квантора forall

следовательно вопрос: можно ли в функции из двух аргументов сделать тайп аппликейшн только по второму?

можно

с помощью улитки

о, точно

спасибо

если бы у нас были бы тайплевел лямбды, то можно было бы и swap функцию написать в общем случае, а не как сейчас

а там гарантированно всегда будет тайп-апп только по второму?

если да, то вот для этого как раз {} и нужен

или можно поменять аргументы в forall местами (работает только в некоторых случаях)

не уверен

{} нужно чтобы запретить тайпапп или же чтобы не писать улитку лишний раз?

просто я не могу придумать кейс где нужно намеренно запрещать тайпапп по переменной

тайпапп нужен обычно когда типоаргумент не может вывестись из аргументов

ну или когда мы какой-нить Symbol хотим прокинуть или что-то еще

поэтому использовать тайпапп когда он выводится обычно не нужно

протащить на тайп левеле какую-то инфу