Iceland_jack

This is to say that (length-indexed) "Arrays" are Representable functors[1]. A `Vec n a` is isomorphic to (Fin n -> a), where Fin n = { x :: Nat | x < n }.

  instance pi n. Representable (Vec n) where
    type Rep (Vec n) = Fin n
    index :: Vec n a -> (Fin n -> a)
    index = ..
    tabulate :: (Fin n -> a) -> Vec n a
    tabulate = ..

[1] https://hackage-content.haskell.org/package/adjunctions-4.4....

To your point, but lispers like the author of Let Over Lambda specifically called Lisp non-functional.

Maybe you meant to write

    (??) :: Functor f => f (a -> b) -> a -> f b
    funs ?? a = fmap ($ a) funs

from lens: https://hackage.haskell.org/package/lens-5.3.2/docs/Control-...

This is valid definition of lift along a different, less interesting but more general axis.

    lift = (??) @[]

> 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 ($))
    = ($)

lift = sequenceA @[] @(a ->)

I appreciate the link to https://dl.acm.org/doi/10.1145/3236774

Haskell focuses on both, but prioritizes research. I have had several Haskell jobs and highly recommend it for the personal enjoyment.

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/...

In Haskell behavour is type-directed (type classes) and they describe both.

What does that mean?

I met Sam Derbyshire at ZuriHac who told me all the difficult architectural work had been done for SIMD support.

+ https://gitlab.haskell.org/ghc/ghc/-/issues/7741

It might make it for GHC 9.12 (for 128 bit vectors only, and mostly floating-point operations unless other people come in and contribute).

The patch is at:

+ https://gitlab.haskell.org/ghc/ghc/-/merge_requests/12860

I write this in my Haskell day job every day.

That reminds me, I should write a Monad tutorial.

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

With https://ucsd-progsys.github.io/liquidhaskell/, but as a separate checker. I think there are talks of integrating it into the compiler

See "Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell" by Simon Peyton Jones

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

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

What's the big deal, using a font outside of its narrowly designed purpose is certainly not it. Some people venture outside the box

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,

Notions of Computation as Monoids https://www.fceia.unr.edu.ar/~mauro/pubs/Notions_of_Computat...

You would be surprised how much Haskell is practical for boring stuff, try it out http://learnyouahaskell.com/

What do you mean by 'open ended', are you talking about literals for data structures or something deeper?

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

Don't learn it from HN (clueless)

Separating IO is kind of the killer feature, something like `rand()` is not an int unless you're reading dilbert[1] or xkcd[2]. Basic equations break down in the face of an Int-valued IO-action being conflated with an Int

[1] https://dilbert.com/search_results?terms=Random+Number+Gener... [2] https://xkcd.com/221/