Iceland_jack

6 か月前議論

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

Iceland_jack

7 か月前議論

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

Iceland_jack

2 年前議論

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 = (??) @[]

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

What does that mean?

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

I write this in my Haskell day job every day.

Iceland_jack

2 年前議論

That reminds me, I should write a Monad tutorial.

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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

Iceland_jack

2 年前議論

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)

Iceland_jack

3 年前議論

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.

Iceland_jack

投稿

Haskell: Pattern Synonyms

コメント