おきしみみ (oxij) wrote,
おきしみみ
oxij

Обратные функции и паттерн-матчинг

Пусть у нас есть функция-примитив cons с типом forall a . a -> [a] -> [a] (любители System F могут отбросить часть до точки).
А также функции head с типом forall a . [a] -> a и tail с типом forall a . [a] -> [a].

Тогда Хаскелевский оператор (:) можно чудесным образом реализовать как:
(:) a b = cons a b

Изоморфный ему в uncurry форме:
(:) (a,b) = cons a b

или:
(:) t = cons (fst t) (snd t)


Элементарно, да? Забавная мысль заключается в том, что, если посмотреть на левую часть определения функции:
sumall [] = 0
sumall (a:b) = a + sumall b

то там написана обратная функция к (:):
(:)' l = (head l, tail l)


А потому, если предоставить юзеру возможность определять свои обратные функции, то из всех паттерн-матчингов можно оставить только распаковку таплов, а остальные операции сводить к этой. Тогда доступным удовольствием, например, является радость жизни с программами а-ля:
sumallStack emptyStack = 0
sumallStack (a `push` s) = a + sumallStack s


Дальше мне разговляться на эту тему лень, но замечу, что слева от знака равно стоит не совсем обратная функция, а предикат с обратной функцией, но это не суть важно. Главное то, что меня иногда жутко тянет заиметь такую фичу, чтобы оборачивать в клёвый синтаксический сахар всякие премудрые упаковки/распаковки/etc.
И ещё замечу, что в языках с какими-нибудь зависимыми типами, например, можно даже попытать счастья в доказательстве того, что композиция обратной функции и её прямой версии есть id.
Tags: haskell
Subscribe
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 8 comments