DF
Понятно
Size: a a a
2020 May 23
Oℕ
ну @kremovtort видимо имел в виду, что писать на идрисе как в пейпере wfpm нельзя
почему
λ
так че с модульностью в завтипах-то?
Ну вот @clayrat говорит, что перспективы лени в завтипах крайне туманны
AA
почему
потому что ленивости нет
Oℕ
потому что ленивости нет
но ведь можно писать, как в пейпере описано
AA
но ведь можно писать, как в пейпере описано
но работать-то будет не как в пейпере написано
R
{A : Type} -> {F : A -> Type} -> {G: (a :A) -> F a -> Type} ->
( f: (a :A) -> F a ) ->
( (a : A) -> (fa : F a) -> G a fa) ->
a -> G a ( f a)то есть самый общий? Окей,
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
(f -< h >- g) (a , b) (c , d) = h (f a c) (g b d) имеет вот такой тип (это по-моему даже не самый общий):_-<_>-_ : ∀ {α β γ δ ε ζ η} {A : Set α} {B : A -> Set β} {C : A -> Set γ}
{D : ∀ {a a'} -> B a -> C a' -> Set δ} {E : ∀ {a} -> C a -> Set ε}
{F : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} -> D b c -> E c' -> Set ζ}
{G : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c} {e : E c'}
-> F d e -> Set η}
-> (f : ∀ a -> (c : C a) -> E c)
-> (∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c}
-> (e : E c') -> (f : F d e) -> G f)
-> (g : ∀ {a a'} {c : C a} -> (b : B a') -> (d : D b c) -> F d (f a c))
-> (p : Σ A B)
-> (q : Σ (C _) (D _))
-> G (g _ _)я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
R
Oℕ
то есть самый общий? Окей,
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
(f -< h >- g) (a , b) (c , d) = h (f a c) (g b d) имеет вот такой тип (это по-моему даже не самый общий):_-<_>-_ : ∀ {α β γ δ ε ζ η} {A : Set α} {B : A -> Set β} {C : A -> Set γ}
{D : ∀ {a a'} -> B a -> C a' -> Set δ} {E : ∀ {a} -> C a -> Set ε}
{F : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} -> D b c -> E c' -> Set ζ}
{G : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c} {e : E c'}
-> F d e -> Set η}
-> (f : ∀ a -> (c : C a) -> E c)
-> (∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c}
-> (e : E c') -> (f : F d e) -> G f)
-> (g : ∀ {a a'} {c : C a} -> (b : B a') -> (d : D b c) -> F d (f a c))
-> (p : Σ A B)
-> (q : Σ (C _) (D _))
-> G (g _ _)я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
но вопрос же не про агду был
λ
Oℕ
то есть самый общий? Окей,
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
(f -< h >- g) (a , b) (c , d) = h (f a c) (g b d) имеет вот такой тип (это по-моему даже не самый общий):_-<_>-_ : ∀ {α β γ δ ε ζ η} {A : Set α} {B : A -> Set β} {C : A -> Set γ}
{D : ∀ {a a'} -> B a -> C a' -> Set δ} {E : ∀ {a} -> C a -> Set ε}
{F : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} -> D b c -> E c' -> Set ζ}
{G : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c} {e : E c'}
-> F d e -> Set η}
-> (f : ∀ a -> (c : C a) -> E c)
-> (∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c}
-> (e : E c') -> (f : F d e) -> G f)
-> (g : ∀ {a a'} {c : C a} -> (b : B a') -> (d : D b c) -> F d (f a c))
-> (p : Σ A B)
-> (q : Σ (C _) (D _))
-> G (g _ _)я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
2 . ну это ещё вопрос, какая это нагрузка
Oℕ
то есть самый общий? Окей,
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
(f -< h >- g) (a , b) (c , d) = h (f a c) (g b d) имеет вот такой тип (это по-моему даже не самый общий):_-<_>-_ : ∀ {α β γ δ ε ζ η} {A : Set α} {B : A -> Set β} {C : A -> Set γ}
{D : ∀ {a a'} -> B a -> C a' -> Set δ} {E : ∀ {a} -> C a -> Set ε}
{F : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} -> D b c -> E c' -> Set ζ}
{G : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c} {e : E c'}
-> F d e -> Set η}
-> (f : ∀ a -> (c : C a) -> E c)
-> (∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c}
-> (e : E c') -> (f : F d e) -> G f)
-> (g : ∀ {a a'} {c : C a} -> (b : B a') -> (d : D b c) -> F d (f a c))
-> (p : Σ A B)
-> (q : Σ (C _) (D _))
-> G (g _ _)я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
и как 2 относится к вопросу?
Oℕ
то есть самый общий? Окей,
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
1. в агде это не самый общий, вселенные тоже могут зависеть от значений
2. это большая нагрузка на компилятор. Потому что выражение чуть посложнее типа
(f -< h >- g) (a , b) (c , d) = h (f a c) (g b d) имеет вот такой тип (это по-моему даже не самый общий):_-<_>-_ : ∀ {α β γ δ ε ζ η} {A : Set α} {B : A -> Set β} {C : A -> Set γ}
{D : ∀ {a a'} -> B a -> C a' -> Set δ} {E : ∀ {a} -> C a -> Set ε}
{F : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} -> D b c -> E c' -> Set ζ}
{G : ∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c} {e : E c'}
-> F d e -> Set η}
-> (f : ∀ a -> (c : C a) -> E c)
-> (∀ {a a' a''} {b : B a} {c : C a'} {c' : C a''} {d : D b c}
-> (e : E c') -> (f : F d e) -> G f)
-> (g : ∀ {a a'} {c : C a} -> (b : B a') -> (d : D b c) -> F d (f a c))
-> (p : Σ A B)
-> (q : Σ (C _) (D _))
-> G (g _ _)я не хочу, чтобы мой компилятор такое выводил (но я бы не отказался, если бы в компилятор была встроена тулза, которая генерирует такой код, типа как Agsy в агде)
3. в большинстве случаев когда люди хотят вывод типов, они думают о хиндли-милнере, а не зависимых типах
итого: выводить зависимые полиморфные типы — это медленно, непонятно, насколько общие типы выводить и в итге все равно будет контринтуитивно. Этим должна встроенная в компилятор тулза заниматься, которая код генерирует, а не тайпчекер
3 при чём тут люди?
R
но вопрос же не про агду был
я не люблю, когда язык меня ограничивает, соответственно идрис я как-то более-менее всерьез не рассматриваю, слишком уж он убогий для зависимо-типизированного программирования (может идрис 2 получше, не знаю)
Oℕ
я не люблю, когда язык меня ограничивает, соответственно идрис я как-то более-менее всерьез не рассматриваю, слишком уж он убогий для зависимо-типизированного программирования (может идрис 2 получше, не знаю)
чем вас ограничивает идрис?
Oℕ
но ведь кроме идриса и агды есть много других языков
R
чем вас ограничивает идрис?
говеный инференс, нельзя явно указывать вселенные
Oℕ
говеный инференс, нельзя явно указывать вселенные
а где вас не устроил инференс вселенных, расскажите
R
не вселенных инференс, а неявных аргументов, в смысле
R
я как-то пытался перетащить проект с агды на идрис. Поматерился день и забил