( Редактировать 1: Я пропустил пару компонентов вашего вопроса в первый раз; см. Нижнюю часть моего ответа.)
Способ думать о такого рода утверждениях - смотреть на типы. Форма аргумента, которую вы имеете, называется силлогизмом; однако, я думаю, что вы что-то неправильно запоминаете. Существует много разных видов силлогизмов, и ваш, насколько я могу судить, не соответствует составу функций. Давайте рассмотрим вид силлогизма, который делает:
- Если будет солнечно, мне станет жарко.
- Если мне станет жарко, я пойду купаться.
- Поэтому, , если будет солнечно, я пойду поплавать.
Это называется гипотетическим силлогизмом . В логических терминах мы бы написали это следующим образом: пусть S означает предложение "солнечно", пусть H означает предложение "Я буду жарко", и пусть W означает предложение "Я пойду купаться". Запись α → β для " α подразумевает β " и запись ∴ для "следовательно", мы можем перевести вышеприведенное в:
- S → H
- В → Ш
- ∴ S → W
Конечно, это работает, если мы заменим S , H и W на любые произвольные α , β и γ . Теперь это должно выглядеть знакомо. Если мы поменяем стрелку импликации → на стрелку функции ->, это станет
a -> bb -> c- ∴
a -> c
И вот, у нас есть три компонента типа оператора композиции! Чтобы думать об этом как о логическом силлогизме, вы можете рассмотреть следующее:
- Если у меня есть значение типа
a, я могу получить значение типа b.
- Если у меня есть значение типа
b, я могу получить значение типа c.
- Следовательно, , если у меня есть значение типа
a, я могу получить значение типа c.
Это должно иметь смысл: в f . g существование функции g :: a -> b говорит вам, что предпосылка 1 верна, а f :: b -> c говорит вам, что предпосылка 2 верна. Таким образом, вы можете заключить последнее утверждение, для которого функция f . g :: a -> c является свидетелем.
Я не совсем уверен, что переводит твой силлогизм. Это почти экземпляр modus ponens , но не совсем. Аргументы Modus Ponens имеют следующую форму:
- Если идет дождь, тогда я промокну.
- Идет дождь.
- Следовательно, Я промокну.
Запись R для "идет дождь" и W для "Я промокну", это дает нам логическую форму
- R → W
- ∴ Ш
Замена стрелки импликации на стрелку функции дает нам следующее:
a -> ba- ∴
b
И это просто функциональное приложение, как мы видим из типа ($) :: (a -> b) -> a -> b. Если вы хотите рассматривать это как логический аргумент, он может иметь форму
- Если у меня есть значение типа
a, я могу получить значение типа b.
- У меня есть значение типа
a.
- Следовательно, Я могу получить значение типа
b.
Здесь рассмотрим выражение f x. Функция f :: a -> b является свидетельством истинности суждения 1; значение x :: a является свидетельством истинности предложения 2; и, следовательно, результат может быть типа b, что доказывает заключение. Это именно то, что мы нашли из доказательства.
Теперь ваш оригинальный силлогизм принимает следующую форму:
- Все мальчики - люди.
- Али - мальчик.
- Следовательно, Али - это человек.
Давайте переведемэто к символам. Bx будет обозначать, что x мальчик; Hx будет означать, что x является человеком; a будет обозначать Али; и 12 x . φ говорит, что φ верно для всех значений x . Тогда у нас есть
- ∀ х . Bx → Hx
- Ba
- ∴ Ха
Это почти modus ponens, но оно требует создания экземпляра. Хотя логически верно, я не уверен, как интерпретировать это на уровне системы типов; если кто-то хочет помочь, я весь в ушах. Одно предположение было бы типом ранга 2 как (forall x. B x -> H x) -> B a -> H a, но я почти уверен, что это неправильно. Другим предположением может быть более простой тип, например (B x -> H x) -> B Int -> H Int, где Int обозначает Али, но, опять же, я почти уверен, что это неправильно. Опять же: если вы знаете, пожалуйста, дайте мне знать тоже!
И последнее замечание. Взгляд на вещи таким образом - следуя связи между доказательствами и программами - в конечном итоге приводит к глубокой магии изоморфизма Карри-Ховарда , но это более сложная тема. (Хотя это действительно круто!)
Редактировать 1: Вы также запросили пример композиции функции. Вот один пример. Предположим, у меня есть список отчеств людей. Мне нужно составить список всех средних инициалов, но для этого мне сначала нужно исключить все несуществующие вторые имена. Легко исключить всех, чье второе имя пусто; мы просто включаем всех, чье отчество не null с filter (\mn -> not $ null mn) middleNames. Точно так же мы можем легко получить чью-то среднюю букву с head, и поэтому нам просто нужно map head filteredMiddleNames, чтобы получить список. Другими словами, у нас есть следующий код:
allMiddleInitials :: [Char]
allMiddleInitials = map head $ filter (\mn -> not $ null mn) middleNames
Но это раздражающе специфично; мы действительно хотим функцию генерации среднего начального значения. Итак, давайте изменим это на один:
getMiddleInitials :: [String] -> [Char]
getMiddleInitials middleNames = map head $ filter (\mn -> not $ null mn) middleNames
Теперь давайте посмотрим на что-нибудь интересное. Функция map имеет тип (a -> b) -> [a] -> [b], а поскольку head имеет тип [a] -> a, map head имеет тип [[a]] -> [a]. Аналогично, filter имеет тип (a -> Bool) -> [a] -> [a], и поэтому filter (\mn -> not $ null mn) имеет тип [a] -> [a]. Таким образом, мы можем избавиться от параметра и вместо этого написать
-- The type is also more general
getFirstElements :: [[a]] -> [a]
getFirstElements = map head . filter (not . null)
И вы видите, что у нас есть бонусный экземпляр композиции: not имеет тип Bool -> Bool, а null имеет тип [a] -> Bool, поэтому not . null имеет тип [a] -> Bool: он сначала проверяет, является ли данный список пуст, и затем возвращает, является ли это не . Это преобразование, кстати, изменило функцию в стиль без точек ; то есть результирующая функция не имеет явных переменных.
Вы также спрашивали о "сильной привязке". Я думаю, что вы имеете в виду приоритет операторов . и $ (и, возможно, приложения-функции). В Haskell, как и в арифметике, некоторые операторы имеют более высокий приоритет, чем другие, и, следовательно, связываются более тесно. Например, в выражении 1 + 2 * 3 это анализируется как 1 + (2 * 3). Это связано с тем, что в Haskell действуют следующие декларации:
infixl 6 +
infixl 7 *
Чем выше число (уровень приоритета), тем быстрее вызывается этот оператор, и, следовательно, чем теснее оператор связывается. Применение функций фактически имеет бесконечный приоритет, поэтому оно связывается наиболее плотно: выражение f x % g y будет анализироваться как (f x) % (g y) для любого оператора %. Операторы . (состав) и $ (приложение) имеют следующие объявления исправления:
infixr 9 .
infixr 0 $
Уровни приоритета варьируются от нуля до девяти, поэтому здесь говорится, что оператор . связывает больше плотно, чем любой другой (кроме приложения функции), а $ связывает меньше плотно. Таким образом, выражение f . g $ h будет анализироваться как (f . g) $ h; и фактически для большинства операторов f . g % h будет (f . g) % h, а f % g $ h будет f % (g $ h). (Единственными исключениями являются несколько редких других операторов с нулевым или девятью приоритетами.)