Исправление quasimoto, (текущая версия) :
Очевидно, что не нужно, т.к. редуцировать их нельзя.
Можно — что в обычном лямбда исчислении (см. Barendregt — 3 глава, отношение редукции определяется на множестве всех лямбда-термов (открытых и закрытых), которое обозначается как Λ (2 глава), множество закрытых термов обозначается как Λ⁰ — отношение редукции задаётся не на нём, хотя вполне на него сужается), что в агде:
f = λ x → let y = x in let z = x; a₁ = replicate {n = y} 1 in let a₂ = replicate {n = z} 2 in a₁ , a₂
-- C-c C-n f (i.e. normal form of `f`)
-- =>
-- λ x → replicate 1 Σ., replicate 2
f′ : (x : ℕ) → Vec ℕ x × Vec ℕ x
f′ = λ x → replicate 1 , replicate 2
-- C-c C-n f′
-- =>
-- λ x → replicate 1 Σ., replicate 2
record Proxy {A : Set} (_ : A) : Set where
check-f : Proxy f
check-f = record {}
-- C-c C-d check-f (i.e. type of `check-f`)
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
check-f′ : Proxy f′
check-f′ = record {}
-- C-c C-d check-f′
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
-- C-c C-n Proxy f (i.e. normal form of _type_ `Proxy f`)
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
-- C-c C-n Proxy f′
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
И где тут редукция?
5!≡12*10 : 5 ! ≡ 12 * 10
5!≡12*10 = refl
-- C-c C-n 5 !
-- =>
-- 120
-- C-c C-n 12 * 10
-- =>
-- 120
-- C-c C-d 5!≡12*10
-- =>
-- 120 ≡ 120
-- C-c C-n 5 ! ≡ 12 * 10
-- =>
-- 120 ≡ 120
Особенно во втором случае
Я уже два раза рассказывал про то как работает индукция (рекурсия) с зависимым паттерн-матчингом:
a+0≡a : ∀ a → a + 0 ≡ a
a+0≡a 0 = refl
--
-- Base case, a ~ 0:
--
-- C-c C-n 0 + 0 ≡ 0
-- =>
-- 0 ≡ 0
--
-- C-c C-d refl
-- =>
-- _x_76 ≡ _x_76
--
-- s.t. refl : 0 ≡ 0 is w.t.
--
a+0≡a (suc a) = cong suc (a+0≡a a)
--
-- Step case, a ~ suc a:
--
-- C-c C-n λ a → suc a + 0 ≡ suc a
-- =>
-- λ a → suc (a + 0) ≡ suc a
--
-- C-c C-d λ a → cong suc (a+0≡a a)
-- =>
-- (a : ℕ) → suc (a + 0) ≡ suc a
--
-- C-c C-n (a : ℕ) → suc (a + 0) ≡ suc a
-- =>
-- itself
--
-- s.t.
--
-- ... | suc a = cong suc (a+0≡a a) <- induction/recursion in (dep.) p.m. case.
-- ^ : a + 0 ≡ a
-- i.e. w.t. as well.
Оно есть в самом определении «статической системы типов».
Вот LF это «теория типов», а не «система типов» — ей действительно всё равно, в её абстрактных рамках индексация действительно проводится «любыми» термами, безотносительно каких-то стадий (стадий нет, есть отношения на множествах термов, типов и т.п. — где у Barendregt или Lambek & Scott стадии?), но конкретная «система типов» вместе с реальным языком с «системой эффектов» вполне могут быть построены вокруг LF так, что всё ей (LF) свойственное будет работать исключительно с constexpr типами, или «хуже» — это может быть голый пруф/тайп-чекер LF без рантайма (но с этими самыми тотальными редукциями термов в типах, считаем за CTFE) и он _будет_ реализацией «теории типов» LF.
Это не типы.
http://i.imgur.com/C3a9Bem.png — я про «types:».
More formally
Ты приводишь что я просил? То есть «Термы являются типами»?
Ну ладно, ты всё ещё говоришь про то, что индексация должна проводится «любыми термами». Я этого не понимаю.
Никакого ИО мы не рассматирваем
Ну вот и чекай concat и т.п. как в той же агде — из ИО ничего не прилетает, значит всё известно, проблем нет?
А как ты сформулируешь понятие «статически типизированный язык» если у тебя нету понятий компайлтайма и рантайма?
Но они есть — в C++/D/Agda. Как и редукции термов в типах. В Agda можно считать, что compile-time это проверка типов (с тотальными редукциями), потом (тотальное же) вычисление нормальных форм, в том числе терма main типа IO T, а runtime это интерпретация этого терма main самим RTS (с частичными вычислениями).
но тогда ВАЖНО когда происходят редукции, а когда - тайпчек
А когда происходит вычисление constexpr функций в C++? Или CTFE в D?
пишется в простой типизированной лямбде
Этого тоже не понимаю. Вот в Haskell 2010 не пишется — пробовали же вроде тут.
Что такое эти квалификаторы? Явно не типы. И не кайнды. И вообще у тебя не получится сформулировать корректную систему типов с такими квалификаторами.
Квалификаторы это проблема, вообще-то — следствие отсутствия системы эффектов / patriality (раз мы хотим вычисления в compile-time, нужно как-то отражать тотальность, аналогично чистоте) в языке, а с ними всё уже вполне формулируется (грубо говоря constexpr T -> T; T const[&] -> IO T; T[&] -> IO (Ref T), снаружи IO/Partiality у нас применимо CTFE).
Ничем не проще.
Исправление quasimoto, :
Очевидно, что не нужно, т.к. редуцировать их нельзя.
Можно — что в обычном лямбда исчислении (см. Barendregt — 3 глава, отношение редукции определяется на множестве всех лямбда-термов (открытых и закрытых), которое обозначается как Λ (2 глава), множество закрытых термов обозначается как Λ⁰ — отношение редукции задаётся не на нём, хотя вполне на него сужается), что в агде:
f = λ x → let y = x in let z = x; a₁ = replicate {n = y} 1 in let a₂ = replicate {n = z} 2 in a₁ , a₂
-- C-c C-n f (i.e. normal form of `f`)
-- =>
-- λ x → replicate 1 Σ., replicate 2
f′ : (x : ℕ) → Vec ℕ x × Vec ℕ x
f′ = λ x → replicate 1 , replicate 2
-- C-c C-n f′
-- =>
-- λ x → replicate 1 Σ., replicate 2
record Proxy {A : Set} (_ : A) : Set where
check-f : Proxy f
check-f = record {}
-- C-c C-d check-f (i.e. type of `check-f`)
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
check-f′ : Proxy f′
check-f′ = record {}
-- C-c C-d check-f′
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
-- C-c C-n Proxy f (i.e. normal form of _type_ `Proxy f`)
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
-- C-c C-n Proxy f′
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
И где тут редукция?
5!≡12*10 : 5 ! ≡ 12 * 10
5!≡12*10 = refl
-- C-c C-n 5 !
-- =>
-- 120
-- C-c C-n 12 * 10
-- =>
-- 120
-- C-c C-d 5!≡12*10
-- =>
-- 120 ≡ 120
-- C-c C-n 5 ! ≡ 12 * 10
-- =>
-- 120 ≡ 120
Особенно во втором случае
Я уже два раза рассказывал про то как работает индукция (рекурсия) с зависимым паттерн-матчингом:
a+0≡a : ∀ a → a + 0 ≡ a
a+0≡a 0 = refl
--
-- Base case, a ~ 0:
--
-- C-c C-n 0 + 0 ≡ 0
-- =>
-- 0 ≡ 0
--
-- C-c C-d refl
-- =>
-- _x_76 ≡ _x_76
--
-- s.t. refl : 0 ≡ 0 is w.t.
--
a+0≡a (suc a) = cong suc (a+0≡a a)
--
-- Step case, a ~ suc a:
--
-- C-c C-d λ a → cong suc (a+0≡a a)
-- =>
-- (a : ℕ) → suc (a + 0) ≡ suc a
--
-- C-c C-n (a : ℕ) → suc (a + 0) ≡ suc a
-- =>
-- itself
--
-- s.t.
--
-- ... | suc a = cong suc (a+0≡a a) <- induction/recursion in (dep.) p.m. case.
-- ^ : a + 0 ≡ a
-- i.e. w.t. as well.
Оно есть в самом определении «статической системы типов».
Вот LF это «теория типов», а не «система типов» — ей действительно всё равно, в её абстрактных рамках индексация действительно проводится «любыми» термами, безотносительно каких-то стадий (стадий нет, есть отношения на множествах термов, типов и т.п. — где у Barendregt или Lambek & Scott стадии?), но конкретная «система типов» вместе с реальным языком с «системой эффектов» вполне могут быть построены вокруг LF так, что всё ей (LF) свойственное будет работать исключительно с constexpr типами, или «хуже» — это может быть голый пруф/тайп-чекер LF без рантайма (но с этими самыми тотальными редукциями термов в типах, считаем за CTFE) и он _будет_ реализацией «теории типов» LF.
Это не типы.
http://i.imgur.com/C3a9Bem.png — я про «types:».
More formally
Ты приводишь что я просил? То есть «Термы являются типами»?
Ну ладно, ты всё ещё говоришь про то, что индексация должна проводится «любыми термами». Я этого не понимаю.
Никакого ИО мы не рассматирваем
Ну вот и чекай concat и т.п. как в той же агде — из ИО ничего не прилетает, значит всё известно, проблем нет?
А как ты сформулируешь понятие «статически типизированный язык» если у тебя нету понятий компайлтайма и рантайма?
Но они есть — в C++/D/Agda. Как и редукции термов в типах. В Agda можно считать, что compile-time это проверка типов (с тотальными редукциями), потом (тотальное же) вычисление нормальных форм, в том числе терма main типа IO T, а runtime это интерпретация этого терма main самим RTS (с частичными вычислениями).
но тогда ВАЖНО когда происходят редукции, а когда - тайпчек
А когда происходит вычисление constexpr функций в C++? Или CTFE в D?
пишется в простой типизированной лямбде
Этого тоже не понимаю. Вот в Haskell 2010 не пишется — пробовали же вроде тут.
Что такое эти квалификаторы? Явно не типы. И не кайнды. И вообще у тебя не получится сформулировать корректную систему типов с такими квалификаторами.
Квалификаторы это проблема, вообще-то — следствие отсутствия системы эффектов / patriality (раз мы хотим вычисления в compile-time, нужно как-то отражать тотальность, аналогично чистоте) в языке, а с ними всё уже вполне формулируется (грубо говоря constexpr T -> T; T const[&] -> IO T; T[&] -> IO (Ref T), снаружи IO/Partiality у нас применимо CTFE).
Ничем не проще.
Исходная версия quasimoto, :
Очевидно, что не нужно, т.к. редуцировать их нельзя.
Можно — что в обычном лямбда исчислении (см. Barendregt — 3 глава, отношение редукции определяется на множестве всех лямбда-термов (открытых и закрытых), которое обозначается как Λ (2 глава), множество закрытых термов обозначается как Λ⁰ — отношение редукции задаётся не на нём, хотя вполне на него сужается), что в агде:
f = λ x → let y = x in let z = x; a₁ = replicate {n = y} 1 in let a₂ = replicate {n = z} 2 in a₁ , a₂
-- C-c C-n f (i.e. normal form of `f`)
-- =>
-- λ x → replicate 1 Σ., replicate 2
f′ : (x : ℕ) → Vec ℕ x × Vec ℕ x
f′ = λ x → replicate 1 , replicate 2
-- C-c C-n f′
-- =>
-- λ x → replicate 1 Σ., replicate 2
record Proxy {A : Set} (_ : A) : Set where
check-f : Proxy f
check-f = record {}
-- C-c C-d check-f (i.e. type of `check-f`)
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
check-f′ : Proxy f′
check-f′ = record {}
-- C-c C-d check-f′
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
-- C-c C-n Proxy f (i.e. normal form of _type_ `Proxy f`)
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
-- C-c C-n Proxy f′
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)
И где тут редукция?
5!≡12*10 : 5 ! ≡ 12 * 10
5!≡12*10 = refl
-- C-c C-n 5 !
-- =>
-- 120
-- C-c C-n 12 * 10
-- =>
-- 120
-- C-c C-d 5!≡12*10
-- =>
-- 120 ≡ 120
-- C-c C-n 5 ! ≡ 12 * 10
-- =>
-- 120 ≡ 120
Особенно во втором случае
Я уже два раза рассказывал про то как работает индукция (рекурсия) с зависимым паттерн-матчингом:
a+0≡a : ∀ a → a + 0 ≡ a
a+0≡a 0 = refl
--
-- Base case, a ~ 0:
--
-- C-c C-n 0 + 0 ≡ 0
-- =>
-- 0 ≡ 0
--
-- C-c C-d refl
-- =>
-- _x_76 ≡ _x_76
--
-- s.t. refl : 0 ≡ 0 is w.t.
--
a+0≡a (suc a) = cong suc (a+0≡a a)
--
-- Step case, a ~ suc a:
--
-- C-c C-d λ a → cong suc (a+0≡a a)
-- =>
-- (a : ℕ) → suc (a + 0) ≡ suc a
--
-- C-c C-n (a : ℕ) → suc (a + 0) ≡ suc a
-- =>
-- itself
--
-- s.t.
--
-- ... | suc a = cong suc (a+0≡a a) <- induction/recursion in (dep.) p.m. case.
-- ^ : a + 0 ≡ a
-- i.e. w.t. as well.
Оно есть в самом определении «статической системы типов».
Вот LF это «теория типов», а не «система типов» — ей действительно всё равно, в её абстрактных рамках индексация действительно проводится «любыми» термами, безотносительно каких-то стадий (стадий нет, есть отношения на множествах термов, типов и т.п. — где у Barendregt или Lambek & Scott стадии?), но конкретная «система типов» вместе с реальным языком с «системой эффектов» вполне могут быть построены вокруг LF так, что всё ей (LF) свойственное будет работает исключительно с constexpr типами, или «хуже» — это может быть голый пруф/тайп-чекер LF без рантайма (но с этими самыми тотальными редукциями термов в типах, считаем за CTFE) и он _будет_ реализацией «теории типов» LF.
Это не типы.
http://i.imgur.com/C3a9Bem.png — я про «types:».
More formally
Ты приводишь что я просил? То есть «Термы являются типами»?
Ну ладно, ты всё ещё говоришь про то, что индексация должна проводится «любыми термами». Я этого не понимаю.
Никакого ИО мы не рассматирваем
Ну вот и чекай concat и т.п. как в той же агде — из ИО ничего не прилетает, значит всё известно, проблем нет?
А как ты сформулируешь понятие «статически типизированный язык» если у тебя нету понятий компайлтайма и рантайма?
Но они есть — в C++/D/Agda. Как и редукции термов в типах. В Agda можно считать, что compile-time это проверка типов (с тотальными редукциями), потом (тотальное же) вычисление нормальных форм, в том числе терма main типа IO T, а runtime это интерпретация этого терма main самим RTS (с частичными вычислениями).
но тогда ВАЖНО когда происходят редукции, а когда - тайпчек
А когда происходит вычисление constexpr функций в C++? Или CTFE в D?
пишется в простой типизированной лямбде
Этого тоже не понимаю. Вот в Haskell 2010 не пишется — пробовали же вроде тут.
Что такое эти квалификаторы? Явно не типы. И не кайнды. И вообще у тебя не получится сформулировать корректную систему типов с такими квалификаторами.
Квалификаторы это проблема, вообще-то — следствие отсутствия системы эффектов / patriality (раз мы хотим вычисления в compile-time, нужно как-то отражать тотальность, аналогично чистоте) в языке, а с ними всё уже вполне формулируется (грубо говоря constexpr T -> T; T const[&] -> IO T; T[&] -> IO (Ref T), снаружи IO/Partiality у нас применимо CTFE).
Ничем не проще.