HN user

Iceland_jack

63 karma

Haskell.

Posts1
Comments62
View on HN

As far as I know it's not possible to get this functionality in Haskell even with clever instance magic

It is possible to fill in basic function bodies based on their type, using ghc-justdoit (https://hackage.haskell.org/package/ghc-justdoit). That's maybe not what you meant, if you are looking for integrating pointfree into Haskell it can be added to ghci or your development environment.

    foo :: ((a -> r) -> r) -> (a -> ((b -> r) -> r)) -> ((b -> r) -> r)
    foo = (…)
In this case I wrote it because I knew about the pattern. Your lift definition is just ($)
      flip \a -> ($ a)
    = flip (&)
    = flip (flip ($))
    = ($)

Any function matching the type

    St -> (a, St)
can viewed as `State St' parameterized over `a'. There are several behaviors that organize such functions, such as Monad which "overloads the semicolon" to work on stateful computations. Another behavior implements a stateful interface: `MonadState St'.
    get :: St -> (St, St)
    put :: St -> (St -> ((), St))
With type classes in Haskell, behaviour is type-directed so in order to reap the benefits we declare a new type.
    {-# Language DerivingVia #-}
    {-# Language GADTSyntax  #-}

    -- get :: My St
    -- put :: St -> My ()
    newtype My a where
      My :: (St -> (a, St)) -> My a
      deriving (Functor, Applicative, Monad, MonadState St, MonadFix)
      via State St

Applicative is n-ary lifting, Functor is a special unary case of Applicative:

    liftA0 :: Applicative f => (a)                -> (f a)
    liftF1 ::     Functor f => (a -> b)           -> (f a -> f b)
    liftA2 :: Applicative f => (a -> b -> c)      -> (f a -> f b -> f c)
    liftA3 :: Applicative f => (a -> b -> c -> d) -> (f a -> f b -> f c -> f d)
    .. where
  liftA0 = pure
  liftF1 = fmap

Monads don't have anything to do with laziness but historically the need for them arose because of laziness. It's the first thing explained in the introduction of Tackling the Awkward Squad:

"Call-by-need (or lazy) languages, such as Haskell, wear a hair shirt because their evaluation order is deliberately unspecified. Suppose that we were to extend Haskell by adding side-effecting “functions” such as printChar. Now consider this list

  xs = [printChar 'a', printChar 'b']
(The square brackets and commas denote a list in Haskell.) What on earth might this mean? In SML, evaluating this binding would print 'a' followed by 'b'. But in Haskell, the calls to printChar will only be executed if the elements of the list are evaluated. For example, if the only use of xs is in the call (length xs), then nothing at all will be printed, because length does not touch the elements of the list.

The bottom line is that laziness and side effects are, from a practical point of view, incompatible. If you want to use a lazy language, it pretty much has to be a purely functional language; if you want to use side effects, you had better use a strict language.

For a long time this situation was rather embarrassing for the lazy community: even the input/output story for purely-functional languages was weak and unconvincing, let alone error recovery, concurrency, etc. Over the last few years, a surprising solution has emerged: the monad. I say “surprising” because anything with as exotic a name as “monad” — derived from category theory, one of the most abstract branches of mathematics — is unlikely to be very useful to red-blooded programmers. But one of the joys of functional programming is the way in which apparently-exotic theory can have a direct and practical application, and the monadic story is a good example. Using monads we have found how to structure programs that perform input/output so that we can, in effect, do imperative programming where that is what we want, and only where we want. Indeed, the IO monad is the unifying theme of these notes."

https://www.microsoft.com/en-us/research/wp-content/uploads/...

By floating the forall., we get another representation type for Void (forall a. a) and `absurd' is one half of that isomorphism :)

    absurd :: Void -> (forall a. a)

    drusba :: (forall a. a) -> Void
    drusba void = void @Void

IO distinguishes execution (of actions) from evaluation (of expressions).

To execute an `action :: IO Ty' for a value of `a :: Ty', you use <-

  do (a :: Ty) <- (action :: IO Ty)
     ..
The 'function' rand is not really a function, but an action. It doesn't make sense to ask which int rand() evaluates to, and we can't equationally reason about rand() as an int. We cannot factor it from `rand() + rand()', or replace it with `2 * rand()' because it is not an int! Haskell is explicit about this, `rand :: IO Int' an action that produces an Int when (effectfully) executed.

The addition of actions doesn't make sense `rand + rand': Num-eric operations do not automatically lift over IO Int.[1] Instead we explicitly write `liftA2 (+) rand rand'. Shorthand for

    do r1 <- rand
       r2 <- rand
       pure (r1 + r2)
where r{1,2} are Ints. The separation between evaluation and execution means we can factor rand out while still executing it twice.
  do let r :: IO Int
         r = rand

     r1 <- r
     r2 <- r
     pure (r1 + r2)
This factors out the 'recipe', not the value it produces. To factor out the result of the IO-action, we just use a single bind/draw <-.
  do r1 <- rand
     pure (r1 + r1)
[1] This can be changed with Applicative lifting:
  {-# Language DerivingVia #-}

  deriving via Ap IO a
    instance Num a => Num (IO a)

The abstract concepts give you the tools to quickly classify a datatype. They are not limited to Haskell and let you ask the right questions of datatypes in any language.

The foundational concept is functoriality, i.e. mapping over the argument of a type. Whether a datatype has an instance of

1. (covariant) Functor

2. Contravariant functor

3. Functor+Contravariant (phantom argument), or

4. neither

says a lot about its structure and tells me what further questions I can ask (what hierarchies I can expect): A datatype can only be a Monad if is covariant. It can only be Divisible and Decidable if it is contravariant. If it is both (3.) then its argument is not used (phantom) and can be mapped to any type. If it is neither (4.) it can be invariant (where the argument appears in both positive and negative position: like the Endo datatype) or a more complicated datatype like GADT, which would require a more complicated functor.

  Either a :: Type -> Type
is a Haskell Functor (endofunctor), mapping (->) to (->).
  Either :: Type -> (Type -> Type)
is not an endofunctor, it maps a type to a type constructor and thus maps (->) to (~>) (natural transformations).

If you uncurried Either, you would also get a non-endofunctor which maps from (-×>) (product category) to (->).

  Either' :: (Type, Type) -> Type
Every function is a functor between equality, since equality satisfies congruence:
  isPrime :: Integer -> Bool
is a functor between (:~:) @Integer an (:~:) @Bool. Boolean negation is a function between "less than or equal" to "greater than or equal" categories; mapping (<=) to (>=):
  not :: Bool -> Bool

I always write existential quantification

  data Showable = forall a. Show a => Showable a
with GADT syntax because it can be confusing for people to infer the type of `Showable' from the above definition when you can write it out
  data Showable where
    Showable :: Show a => a -> Showable
josephcsible is right. `forall.' in that context doesn't play a different role. Rather a variable bound by `forall.' is logically the same as existential quantification if it does not appear in the return type which `a' doesn't:
  Showable :: forall a. Show a => a -> Showable
We will get a proper existential quantifier soon

* https://github.com/ghc-proposals/ghc-proposals/pull/473 * https://richarde.dev/papers/2021/exists/exists.pdf

and then

  length :: forall a. [a] -> Int
can be replaced with
  length :: (exists a. [a]) -> Int
and `Showable' will be isomorphic to the "packed constraint" `exists a. Show a ∧ a', explained in the paper. This is a tupled constraint, not a function: `(Dict (Show a), a)'

algebra of typed composition, a discipline for making definitions, study of universal properties, theory of duality, formal theory of analogy, mathematical model of mathematical models, inherently computational, science of analogy, mathematical study of (abstract) algebras of functions, general mathematical theory of structures,

In the definitional sense it is underwhelming, like with many algebraic structures the diversity of instances leads to interesting results. The behaviour of these instantiations have a completely different character even though they instantiate the same pattern

  replicateM :: Int -> [a]      -> [[a]]
  replicateM :: Int -> Cont r a -> Cont r [a]

  sequenceA :: [IO a]             -> IO [a]
  sequenceA :: Maybe (x -> a)     -> (x -> Maybe a)
  sequenceA :: Map key (Parser a) -> Parser (Map key a)
In fact both of them require only an Applicative pattern (aka n-ary lifting) which is weaker than Monad
  liftA0 :: Applicative f => (a)                -> (f a)
  liftA1 :: Functor     f => (a -> b)           -> (f a -> f b)
  liftA2 :: Applicative f => (a -> b -> c)      -> (f a -> f b -> f c)
  liftA3 :: Applicative f => (a -> b -> c -> d) -> (f a -> f b -> f c -> f d)
  liftA4 :: Applicative f => .. 
  where
    liftA0 = pure
    liftA1 = fmap
but has more interesting properties than Monad. Because there is no dependency between Applicative computations they can be run Concurrently[1] or Backwards[2]. They are also closed under Compose-ition[3]. This is not even mentioning what makes an Applicative or a Monad. Functor instances are unique[4] but a single type constructor can have different law-abiding Applicative instances.[5]

[1] https://hackage.haskell.org/package/async/docs/Control-Concu...

[2] https://hackage.haskell.org/package/transformers-0.6.0.4/doc...

[3] https://hackage.haskell.org/package/base-4.16.3.0/docs/Data-...

[4] https://stackoverflow.com/questions/19774904/are-functor-ins...

[5] https://hackage.haskell.org/package/idiomatic