Как определить функцию на основе ее типа?

#function #haskell

Вопрос:

Я пытаюсь определить простую функцию Хаскелла с типом (m -> n -> l) -> (m -> n) -> m -> l . Я думал , что это нужно определить как f g h x = f g (h x) , но, по-видимому, это не так. Как я мог бы исправить эту функцию?

Комментарии:

1. f g h x = g x (h x)

2. Не могли бы вы объяснить, почему это так?

3. рассуждая о том , как вы можете построить элемент типа l , нам определенно нужна первая функция с типом m -> n -> l , чтобы построить элемент типа l , и для этого требуются два параметра с типами m и n соответственно.

Ответ №1:

Основываясь на подписи, единственной разумной реализацией является:

 f :: (m -> n -> l) -> (m -> n) -> m -> l
f g h x = g x (h x)
 

Это имеет смысл , поскольку нам даны две функции g :: m -> n -> l и h :: m -> n и значение x :: m . Мы должны построить значение с типом l . Единственный способ сделать это-использовать функцию g . Для параметра с типом m мы можем работать x , для второго параметра нам нужно значение типа n , у нас нет такого значения, но мы можем построить его, применив h x . Поскольку h x имеет тип h x :: n , мы, таким образом, можем использовать это в качестве второго параметра для g .

Эта функция уже определена: это частный случай (<*>) :: Applicative f => f (n -> l) -> f n -> f l с f ~ (->) m .

Джинн-это инструмент, который рассуждает о типах и, таким образом, генерирует определения функций на основе своей подписи. Если кто-то запросит с f :: (m -> n -> l) -> (m -> n) -> m -> l , мы получим:

 f :: (m -> n -> l) -> (m -> n) -> m -> l
f a b c = a c (b c)
 

которая является той же функцией (за исключением того, что она использует другие имена переменных).

Ответ №2:

 f :: (m -> n -> l) -> (m -> n) -> m -> l
f    g                h           x  = _
 

Теперь вам нужно каким-то образом использовать аргументы.

    g (_ :: m) (_ :: n) :: l
   h (_ :: m) :: n
   x :: m
 

Обоим g и h нужно значение типа m в качестве их первого аргумента. Что ж, к счастью, у нас есть ровно одно такое значение, так что легко понять, что делать.

    g x (_ :: n) :: l
   h x :: n
   x :: m
 

Так что теперь g все еще нужно значение типа n . И снова нам повезло, потому что обращение h к x нам принесло такую ценность.

    g x (h x) :: l
   h x :: n
   x :: m
 

Хорошо, и теперь у нас есть что-то вроде l того , что нам было нужно!

 f g h x = g x (h x)
 

Ответ №3:

 f :: (m -> n -> l) -> (m -> n) -> m -> l
f    g                h           x  = l
  where
  l = 
 

что может произвести ан l для нас? Только g :

       g
 

который принимает два параметра, an m и an n ,

          m n
 

но где мы можем их достать? Что ж, m у нас уже есть,

   m = x
 

и n мы можем получить от h ,

   n = h
 

который нуждается в m

          m
 

и где мы его возьмем m ? У нас уже есть m !