Телеграмм чат группы rust_offtopic страница 8417

11:53пожаловаться #1

а

Alex Zhukovsky

foo :: (Functor f) => f Int -> f Int

Если я определю foo вот так, то "возвращает нулл когда аргумент нулл" будет неверно

foo :: (Functor f) => f Int -> f Int
foo Nothing = foo (Just 5)

то есть типчики не смогли выразить "возвращает нулл когда аргумент нулл"

11:53пожаловаться #2

а

вот изначальное утверждение

11:54пожаловаться #3

а

Как мне проаннтоировать что "возвращает нулл если аргумент нулл"? Как мне сделать Some(None)?

11:54пожаловаться #4

AZ

Если я определю foo вот так, то "возвращает нулл когда аргумент нулл" будет неверно

foo :: (Functor f) => f Int -> f Int
foo Nothing = foo (Just 5)

то есть типчики не смогли выразить "возвращает нулл когда аргумент нулл"

ну если ты прям так хочешь доказать то можно и это проверить

11:54пожаловаться #5

AZ

interface Functor f => VerifiedFunctor (f : Type -> Type) where
  functorIdentity : {a : Type} -> (g : a -> a) -> ((v : a) -> g v = v) -> (x : f a) -> map g x = x
  functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
                       (g1 : a -> b) -> (g2 : b -> c) ->
                       map (g2 . g1) x = (map g2 . map g1) x

VerifiedFunctor Maybe where
  functorIdentity _ _ Nothing = Refl
  functorIdentity g p (Just x) = rewrite p x in Refl
  functorComposition Nothing g1 g2 = Refl
  functorComposition (Just x) g1 g2 = Refl

11:56пожаловаться #6

AZ

ну вот например так проверяется что мейби от нан это нан, а от джаста это джаст

11:57пожаловаться #7

AZ

по аналогии можно написать для нашего foo

11:57пожаловаться #8

AZ

https://t.me/rust_offtopic/176573

Dollar Føølish

Foo None = None?

Αλεχ Zhukovsky in rust_offtopic

11:57пожаловаться #9

AZ

Если я определю foo вот так, то "возвращает нулл когда аргумент нулл" будет неверно

foo :: (Functor f) => f Int -> f Int
foo Nothing = foo (Just 5)

то есть типчики не смогли выразить "возвращает нулл когда аргумент нулл"

Тогда твоя такая реализация не тайпчекнется

11:59пожаловаться #10

а

Если я определю foo вот так, то "возвращает нулл когда аргумент нулл" будет неверно

foo :: (Functor f) => f Int -> f Int
foo Nothing = foo (Just 5)

то есть типчики не смогли выразить "возвращает нулл когда аргумент нулл"

Хотя если взять более реальный пример

foo :: (Functor f) => f a -> f a

в котором у функции foo нет доступа к конструктору типа "a", то тогда действительно, функция foo будет возвращать None если аргумент None, потому что Some она сделать не сможет

12:02пожаловаться #11

AZ

это тоже вариант, но иногда конкретные типы нам могут быть интересны

12:03пожаловаться #12

В

Вафель in rust_offtopic

const fn() -> i32 {
    let mut vec = Vec::new();
    for i in 0..10 {
        vec.push(i * 2);
    }

    vec.iter().sum()
}

Вот искусственный пример как можно полезно применить вектор в const fn. Но нельзя так как в const fn почему-то запрещены аллокации

Проблема в том что компилятору надо

1) проверить что данные которые были доступны только в компайл-тайме, не утекут в рантайм мёртвыми указателями вперёд (я хз как такое сделать)

2) для этого нужно скомпилировать этот кусок кода и выполнить. Это почти как процедурные макросы...

13:00пожаловаться #13

а

Вафель

Проблема в том что компилятору надо

1) проверить что данные которые были доступны только в компайл-тайме, не утекут в рантайм мёртвыми указателями вперёд (я хз как такое сделать)

2) для этого нужно скомпилировать этот кусок кода и выполнить. Это почти как процедурные макросы...

1) наверное решается тем, чтобы разрешать хранить в результирующих const глобалах только Copy типы. Ведь никакие Copy типы не содержат указателей, хотя это может быть слишком строгое ограничение

13:03пожаловаться #14

В

Вафель in rust_offtopic

1) наверное решается тем, чтобы разрешать хранить в результирующих const глобалах только Copy типы. Ведь никакие Copy типы не содержат указателей, хотя это может быть слишком строгое ограничение

Фанфакт: поинтер это копи тип (пруф)

13:09пожаловаться #15

p

polunin.ai in rust_offtopic

Подскажите дополнительную хеш-функцию для двойного хеширования в хеш-таблице

13:14пожаловаться #16

p

polunin.ai in rust_offtopic

Какую-то попроще