Я кстати до сих пор не очень понимаю почему оно

Question

Я кстати до сих пор не очень понимаю почему оно

работает. В задании было сказано напишите вот такой вот список, ну я и написал, а понимания почему это возможно так и не появилось.
В том примере, насколько я понимаю, у конструктора данных :> типы (a -> b) и FList b c являются экзистенционалными, то есть при паттерн матчинге по конструктору :> списка, мы теряем тип функции и тип оставшегося списка.
Но как тогда работает функция apply? Почему у нас все еще есть возможность применить функцию у которой мы потеряли тип к аргументу?

#haskell #programming #russian

0

18.12.2021

3 ответов

12 просмотров

кана

applyFList :: FList a b -> a -> b applyFList (f :> list) x = applyFList list (f x) рассмотрим типы термов в этом кейсе ----------- f :: a -> c list :: Flist c b x :: a f x :: c applyFList list (f x) :: b applyFList как видно принимает FList a b и a, возвращает b в нашем случае при передаче list мы говорим что "a = c, b = b" если проставить type-applications, то будет явнее applyFList :: forall a b. FList a b -> a -> b applyFList ((f :: a -> c) :> (list :: FList c b)) (x :: a) = let y :: c = f x in applyFList @c @b list y экзист-тип не теряет тип "c" полностью, он сохраняет связь двух аргументов :> (то есть первый аргумент - функция, которая возвращает значение такого же типа, как первый параметр FList второго аргумента :>)

0

18.12.2021

Иван Автор вопроса

кана
applyFList :: FList a b -> a -> b applyFList (f :>...

Все равно не понимаю как он тип c вычисляет до конкретного. Просто a и b это конкретные типы, но путь от а до b может быть построен через огромное кол-во абстрактных промежуточных типов (как в твоем примере тип c) и это как то не укладывается в голове

0

18.12.2021

кана · Accepted Answer

кана

экзистенциональный у нас "c" мы его не теряем, при патмаче у нас есть как раз "c" то есть у нас есть абстрактный неизвестный тип "c" и две значения которые этот тип используют: a -> c и FList c b

0

18.12.2021

169 похожих чатов

Я кстати до сих пор не очень понимаю почему оно

3 ответов

Похожие вопросы