function distinct(array $a): int
{
    return count(array_flip($a));
}