Last active
May 2, 2024 19:34
-
-
Save tfausak/3e5c178bfc50fe78e7c020b086fe7c92 to your computer and use it in GitHub Desktop.
keywords: Haskell applicative lift liftA liftA2 liftAN ap hoist raise boost
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- This whole thing is shamelessly stolen from: | |
-- <https://doisinkidney.com/snippets/nary-uncurry.html>. | |
-- Without flexible instances, GHC complains about the `HasApply` instances: | |
-- | |
-- > Illegal instance declaration for `HasApply a Z`. All instance types must | |
-- > be of the form `(T a1 ... an)` where `a1 ... an` are *distinct type | |
-- > variables*, and each type variable appears at most once in the instance | |
-- > head. | |
-- | |
-- <https://downloads.haskell.org/~ghc/8.6.3/docs/html/users_guide/glasgow_exts.html#extension-FlexibleInstances> | |
{-# LANGUAGE FlexibleInstances #-} | |
-- Without multi-param type classes, GHC complains about the `HasApply` class: | |
-- | |
-- > Too many parameters for class `HasApply`. | |
-- | |
-- It also complains about the instances: | |
-- | |
-- > Illegal instance declaration for `HasApply a Z`. Only one type can be | |
-- > given in an instance head. | |
-- | |
-- <https://downloads.haskell.org/~ghc/8.6.3/docs/html/users_guide/glasgow_exts.html#extension-MultiParamTypeClasses> | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
-- Without type families, GHC complains about the `Function` family: | |
-- | |
-- > Illegal family declaration for `Function`. | |
-- | |
-- <https://downloads.haskell.org/~ghc/8.6.3/docs/html/users_guide/glasgow_exts.html#extension-TypeFamilies> | |
{-# LANGUAGE TypeFamilies #-} | |
module Buoy ( buoy ) where | |
import qualified Control.Applicative as Applicative | |
-- We need to be able to represent natural numbers at the type level. The | |
-- easiest way to do so is with Peano numbers. A natural number is either zero | |
-- (Z) or one plus some other natural number (S). These two types represent | |
-- that. Note that they do not exist on the value level at all. | |
data Z | |
data S n | |
-- We can use a type family to count the number of arguments a function has. | |
-- `Count a` will be `Z` (0), `Count (a -> b)` will be `S Z` (1), and so on. | |
type family Count f where | |
Count (_a -> b) = S (Count b) | |
Count _a = Z | |
-- This type family constructs a function with `n` arguments where each | |
-- argument (and the result) are wrapped in `f`. If `n` is `Z`, then `a` is the | |
-- return type. Otherwise `n` is `S m` and `a` is the parameter type. | |
type family Function f n a where | |
Function f (S n) (a -> b) = f a -> Function f n b | |
Function f Z a = f a | |
-- This is where the magic happens. This class says that `a` is a function that | |
-- has `n` arguments. If `n` is `Z`, then `a` is simply the identity function. | |
-- Otherwise `n` is `S m` and `a` is an interesting function like `a -> b`. | |
class Count a ~ n => HasApply a n where | |
apply :: Applicative.Applicative f => f a -> Function f (Count a) a | |
instance Count a ~ Z => HasApply a Z where | |
apply = id | |
instance HasApply b n => HasApply (a -> b) (S n) where | |
apply f = apply . (f Applicative.<*>) | |
-- And this is where it all comes together. `buoy` can be used as a replacement | |
-- for `liftA2` and friends. Here are some examples: | |
-- | |
-- buoy not (Just True) | |
-- == liftA not (Just True) | |
-- == not <$> Just True | |
-- == Just False | |
-- | |
-- buoy (++) (Just "h") (Just "i") | |
-- == liftA2 mappend (Just "h") (Just "i") | |
-- == mappend <$> Just "h" <*> Just "i" | |
-- == Just "hi" | |
-- | |
-- buoy bool (Just 'f') (Just 't') (Just False) | |
-- == liftA3 bool (Just 'f') (Just 't') (Just False) | |
-- == bool <$> Just 'f' <*> Just 't' <*> Just False | |
-- == Just 'f' | |
-- | |
-- Note that if you try to buoy a polymorphic function it will fail. | |
-- | |
-- >>> buoy (+) (Just 1) (Just 2) | |
-- <interactive>:1:1: error: | |
-- • Non type-variable argument | |
-- in the constraint: HasApply a (Count a) | |
-- (Use FlexibleContexts to permit this) | |
-- • When checking the inferred type | |
-- it :: forall a. | |
-- (HasApply a (Count a), Num a) => | |
-- Function Maybe (Count a) a | |
-- | |
-- If you enable FlexibleContexts you'll get another error. | |
-- | |
-- >>> :set -XFlexibleContexts | |
-- >>> buoy (+) (Just 1) (Just 2) | |
-- <interactive>:3:1: error: | |
-- • Couldn't match expected type ‘Function Maybe (Count a) a’ | |
-- with actual type ‘Function Maybe (Count a0) a0’ | |
-- NB: ‘Function’ is a non-injective type family | |
-- The type variable ‘a0’ is ambiguous | |
-- • In the ambiguity check for the inferred type for ‘it’ | |
-- To defer the ambiguity check to use sites, enable AllowAmbiguousTypes | |
-- When checking the inferred type | |
-- it :: forall a. | |
-- (HasApply a (Count a), Num a) => | |
-- Function Maybe (Count a) a | |
-- | |
-- If you enable AllowAmbiguousTypes it should work. | |
-- | |
-- >>> :set -XAllowAmbiguousTypes | |
-- >>> buoy (+) (Just 1) (Just 2) | |
-- Just 3 | |
buoy | |
:: (Applicative.Applicative f, HasApply b n) | |
=> (a -> b) -> f a -> Function f n b | |
buoy f = apply . fmap f |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment