История изменений
Исправление quasimoto, (текущая версия) :
Массив элементов без элементов - типичная НЁХ
Таки это вполне обычная «идиома», такая же как и «пустой список» (nil в лиспах).
Поэтому в С++ у std::array есть метод empty:
#include <array>
#include <iostream>
int main()
{
std::array<int, 0> xs {{}};
std::cout << "begin = " << xs.begin() << std::endl
<< "end = " << xs.end() << std::endl
<< "empty = " << xs.empty() << std::endl
<< "size = " << xs.size() << std::endl;
}
Аналогично в Scala:
scala> Array()
res1: Array[Nothing] = Array()
scala> Array().length
res2: Int = 0
или в Agda:
open import Data.Nat
data Vec {a} (A : Set a) : ℕ → Set a where
[] : Vec A 0 -- <- вот это
_∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (1 + n)
open import Data.Empty
empty : Vec ⊥ 0 -- <- аналогично Array[Nothing] скалы
empty = []
Исправление quasimoto, :
Массив элементов без элементов - типичная НЁХ
Таки это вполне обычная «идиома», такая же как и «пустой список» (nil в лиспах).
Поэтому в С++ у std::array есть метод empty:
#include <array>
#include <iostream>
int main()
{
std::array<int, 0> xs {{}};
std::cout << "begin = " << xs.begin() << std::endl
<< "end = " << xs.end() << std::endl
<< "empty = " << xs.empty() << std::endl
<< "size = " << xs.size() << std::endl;
}
Аналогично в Scala:
scala> Array()
res1: Array[Nothing] = Array()
scala> Array().length
res2: Int = 0
или в Agda:
open import Data.Nat
data Vec {a} (A : Set a) : ℕ → Set a where
[] : Vec A zero -- <- вот это
_∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
open import Data.Empty
empty : Vec ⊥ 0 -- <- аналогично Array[Nothing] скалы
empty = []
Исходная версия quasimoto, :
Массив элементов без элементов - типичная НЁХ
Таки это вполне обычная «идиома», такая же как и «пустой список» (nil в лиспах).
Поэтому в С++ у std::array есть метод empty:
#include <array>
#include <iostream>
int main()
{
std::array<int, 0> xs {{}};
std::cout << "begin = " << xs.begin() << std::endl
<< "end = " << xs.end() << std::endl
<< "empty = " << xs.empty() << std::endl
<< "size = " << xs.size() << std::endl;
}
Аналогично в Scala:
scala> Array()
res1: Array[Nothing] = Array()
scala> Array().length
res2: Int = 0
или в Agda:
open import Data.Nat
data Vec {a} (A : Set a) : ℕ → Set a where
[] : Vec A zero -- <- вот это
_∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
Vec₀ : Set → Set
Vec₀ A = Vec A 0
empty : Vec₀ ℕ
empty = []