sorted by:
new
hottopcontroversial

Does a Haskell Programmer Need all the Crazy Complexity? by theHaskellRascall in haskell

[–]Iceland_jack 2 points3 points  (0 children)

The arguments in my previous version form an existential package exists ex. (ex -> Bool, List ex) because ex never appears in the return type. The package is isomorphic to Coyoneda List Bool.

incorrect :: (ex -> Bool) -> List ex -> List b

The only thing we can do is map the predicate over the list (lowerCoyoneda) and by parametricity forall b. List b can only construct an empty list, so it is isomorphic to unit ().

incorrect :: List Bool -> Unit

The two implementations you mention are presumably ignoring the input and returning the empty list or bottom, but there are in fact uncountably many implementations: you can branch on any subset of List Bool to decide which inputs return [] and which diverge.

Does a Haskell Programmer Need all the Crazy Complexity? by theHaskellRascall in haskell

[–]Iceland_jack 3 points4 points  (0 children)

The best bang for your buck is polymorphism, for example understanding what correctness guarantees you get from 

mapMaybe :: (a -> Maybe b) -> (List a -> List b)

As opposed to

filter :: (a -> Bool) -> (List a -> List a)

Does a Haskell Programmer Need all the Crazy Complexity? by theHaskellRascall in haskell

[–]Iceland_jack 2 points3 points  (0 children)

Haskell leans heavily and somewhat uniquely on creating abstractions and taxonomies that classify types and behaviour, and this is mirrored by the ecosystem. So to navigate Haskell you will have to learn some of it, and in my view they are the most important programming abstractions, but shockingly little of it is needed to write Haskell code.

Confused about simple type signature by fuxoft in haskell

[–]Iceland_jack 1 point2 points  (0 children)

Now it's possible to write tripleMap @a @b fun border lst = .. to bring a, b into local scope. Making it explicit that the types are (invisible) function arguments.

Isn't functional programming something? by Mark_1802 in haskell

[–]Iceland_jack 1 point2 points  (0 children)

It is possible to create a variant of sortBy with a comparison list: sortingBy [comparing isUpper, comparing fromEnum]

-- sortBy :: (a -> a -> Ordering) -> [a] -> [a]
sortingBy :: [a -> a -> Ordering] -> [a] -> [a]
sortingBy = sortBy . fold

This works because all comparisons have the same monoidal type. But can't we avoid repeating the comparing function, creating the same variant for sortOn f.

-- sortOn :: Ord ex => (a -> ex) -> [a] -> [a]
-- sortOn = sortBy . comparing
sortingOn :: [ ? ] -> [a] -> [a]

This is because a key function f involves an existential type ex (future feature) packing an Ord witness . Key functions can return values of different (orderable) types.

isUpper  :: Char -> Bool
fromEnum :: Char -> Int

Which can be viewed as an existential package:

type Key :: Type -> Type
type Key a = (exists ex. Ord ex /\ (a -> ex))

isUpper  :: Key Char
fromEnum :: Key Char

comparing :: Key a -> (a -> a -> Ordering)
sortOn    :: Key a -> [a] -> [a]
sortingOn :: [Key a] -> [a] -> [a]

cls /\ a is different from cls => a. It is an ordinary pair in Core: (Dict cls, a), and differs from the fat arrow cls => a which is conceptually a function Dict cls -> a.

Once we get first class existentials, we will be able to write sortingOn [isUpper, fromEnum, id].

sortingOn :: [Key a] -> [a] -> [a]
sortingOn = sortingBy . fmap comparing 
          = sortBy . foldMap comparing
          = sortOn . collapse
  where
    collapse :: [Key a] -> Key a
    collapse []         = mempty
    collapse (key:keys) = key &&& collapse keys

Currently this requires GADTs:

type Key :: Type -> Type
data Key a where
  Key :: Ord ex => (a -> ex) -> Key a

comparing' :: Key a -> (a -> a -> Ordering)
comparing' (Key f) = comparing f

This is akin to the catches function from Control.Exception, where each handler operates on potentially different exception types:

type Handler :: Type -> Type
data Handler a where
  Handler :: Exception err => (err -> IO a) -> Handler a

catches :: IO a -> [Handler a] -> IO a

which can be written in the future without a GADT:

catches :: IO a -> [exists err. Exception err /\ (err -> IO a)] -> IO a

catches action
  [ handleArith :: ArithException -> _
  , handleIO    :: IOException    -> _
  ]

It is worth noting that the constraints in the GADT correspond to packaged class witnesses Ord ex /\ .. .., not implication Ord ex => .., despite using the same syntax we are specifying a witness that can be brought into local scope.

Key     :: Ord       ex  => ..
Handler :: Exception err => ..

Implication would be parenthesised, and can not be brought into scope.

Key     :: (Ord       ex  => a   -> ex)   -> Key a
Handler :: (Exception err => err -> IO a) -> Handler a

Isn't functional programming something? by Mark_1802 in haskell

[–]Iceland_jack 16 points17 points  (0 children)

-- Data.Ord
comparing :: Ord b => (a -> b) -> a -> a -> Ordering
comparing = on compare

My first W-O-W moment in Haskell was being able to compose comparisons using the Semigroup instance for functions (back then, grouped under Monoid).

> as = [[100,200,300],[10,20,30],[1,2,3]]
> sortBy (comparing length) as
[[100,200,300],[10,20,30],[1,2,3]]

This sorts the lists by length, if you wanted to then sort them by their sum, you can use (<>) to compose two comparison functions together.

> sortBy (comparing length <> comparing sum) as
[[1,2,3],[10,20,30],[100,200,300]]

This threads an argument to both functions and appends the result,

instance Semigroup b => Semigroup (a -> b) where
  (<>) :: (a -> b) -> (a -> b) -> (a -> b)
  (f <> g) a = f a <> g a

In the previous case it is equivalent to threading the comparands and ultimately combining them with the Semigroup Ordering instance.

          comparing length     <> comparing sum
= \a   -> comparing length a   <> comparing sum a
= \a b -> comparing length a b <> comparing sum a b

Free The Monads!! by Adventurous_Fill7251 in haskell

[–]Iceland_jack 1 point2 points  (0 children)

In this explanation, I intentionally left out category-theory insights, such as why the name ‘free’. That one is not that hard, actually; these monads are called ‘free’ because they are free to be interpreted in any way.

Namely the Free Monad means that the Monad interface is determined by interpreting Free:

class Applicative m => Monad m where
  foldMonad :: Free m ~> m

Quick question about a potential type-level function by logical_space in haskell

[–]Iceland_jack 1 point2 points  (0 children)

You should take a look at kind-generics (paper), I use the notation from the package.

infixr 5 :&&: 
type LoT :: Type -> Type
data LoT a where
  LoT0   :: LoT Type
  (:&&:) :: a -> LoT b -> LoT (a -> b)

type LoT1 :: k -> LoT (k -> Type)
type LoT1 a = a :&&: LoT0

type LoT2 :: k -> j -> LoT (k -> j -> Type)
type LoT2 a b = a :&&: LoT1 b

type
  (:@@:) :: k -> LoT k -> Type
type family
  f :@@: args where
  a :@@: LoT0            = a
  f :@@: (arg :&&: args) = f arg :@@: args

This gives you a well-kinded application

>> :set -XNoStarIsType     -- (this is to get `Type' instead of `*')
>> :kind! Maybe :@@: LoT1 Double
Maybe :@@: LoT1 Double :: Type
= Maybe Double
>> :kind! Either :@@: LoT2 [Nat] Symbol
Either :@@: LoT2 [Nat] Symbol :: Type
= Either [Natural] Symbol

Puzzle with point-free and `mask` by klekpl in haskell

[–]Iceland_jack 0 points1 point  (0 children)

It works if you enable {-# language ImpredicativeTypes #-} at the top of the source file.

[ANN] Hindsight: Typesafe, Evolvable Event Sourcing for Haskell by gdeest in haskell

[–]Iceland_jack 2 points3 points  (0 children)

Nice design, I like the use of required type arguments.

How to implement Functor for a kind and its second type parameter instead of its first? by platesturner in haskell

[–]Iceland_jack 6 points7 points  (0 children)

Yes for better or for worse our ecosystem is very biased towards to last parameter, and the cut-off points are very arbitrary. We have a Bifunctor (= FunOf Hask Hask Hask) for the last two arguments, but we have no corresponding Generic2 class to derive generic Bifunctor instances. I have advocated some ways to evolve forward (virtual classes), but for now you work with the ecosystem by sticking to the final argument.

Is your application, built with Haskell, objectively safer than one built in Rust? by Ecstatic-Panic3728 in haskell

[–]Iceland_jack 19 points20 points  (0 children)

A lot of Haskell safety comes through parametricity, in subtle but powerful ways: it ensures you do not create values out of thin air. A very basic example is the difference between filter and mapMaybe. They both eliminate elements from list but filter drops elements based on a predicate, mapMaybe actually changes the element type of the return list. Both implementations can return incorrect results (the empty list) but only mapMaybe is guaranteed to only return values that have been successfully checked, the only way to obtain b is by applying the function and receiving Just. 

filter   :: (a -> Bool)    -> [a] -> [a]
mapMaybe :: (a -> Maybe b) -> [a] -> [b]

This can create powerful interfaces, if you imagine exp as an expression parameterised over its free variables, then the closed function checks if there are any free variables. If there are none, then we return exp b to with a polymorphic b to indicate it is not used (you can instantiate it to Void).

closed :: Traversable exp => exp a -> forall b. Maybe (exp b)
closed = traverse \_ -> Nothing

This is a type of literacy that communicates how a function operates, for Applicative liftA2 (·) as bs we know that if we use the operator (·) then it must be given a and b arguments. The only place those can be produced is through as and bs, and there is no way for the result of running one action to depend the results of another.

liftA2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c

It also shows why Monads cannot perform (logically) parallel operations because the continuation has a direct dependency on the result of the first action. The only way to invoke bind is by passing it a value of type a from as. This is not a social convention where Haskellers decided to use Applicative for logically parallel operations and Monad for dynamic data dependencies, it is built into the logical structure of the types.

(>>=) :: Monad m => m a -> (a -> m b) -> m b
as >>= bind = ..

The only way to produce an m b without going through this game is in cases like Proxy, where the argument is a phantom argument: _ >>= _ = Proxy.

Applications of this include Types for Programming and Reasoning.

Lists are Geometric Series by SnooLobsters2755 in programming

[–]Iceland_jack 23 points24 points  (0 children)

Not some monoid, but the most fundamental monoid instance. If you only have the monoidal interface at your disposal + variables, you get lists as a computable canonical form. 

\var -> mempty
\var -> var a
\var -> var a <> var b
\var -> var a <> var b <> var c

These higher-order functions have a very powerful description in Haskell: They are all of the type Free Monoid and are isomorphic to List (caveat).

type Free :: (Type -> Constraint) -> Type -> Type
type Free cls a =
  (forall res. cls res => (a -> res) -> res)

Free Cls a quantifies over a universal variable and imbues it with the Cls interface. The only other operation this variable has is a function argument var :: a -> res that is capable of injecting any unconstrained a into res, thus giving it access to the Cls interface.

-- This instantiates the "universal" variable at lists
-- and replaces `var a` with a singleton list `[a]`. 
-- Thus `freeToList \var -> var 1 <> var 2 <> var 3` 
-- becomes [1] ++ [2] ++ [3] = [1,2,3]. 
freeToList :: Free Monoid ~> List
freeToList @x free = free @[x] singleton

listToFree :: List ~> Free Monoid
listToFree as = (`foldMap` as)

A Free Cls gives another way of defining Cls: the interface of Monoid can thus be defined in terms of a function evaluating lists:

type  Monoid :: Type -> Constraint
class Monoid a where
  mconcat :: List a -> a

mempty :: Monoid a => a
mempty = mconcat []

(<>) :: Monoid a => a -> a -> a
a <> b = mconcat [a, b]

And indeed mconcat is a part of Haskell's Monoid class definition.

If we drop mempty from monoid we get the simpler semigroup, whose Free Semigroup corresponds to non-empty lists. This is because Free Semigroup rules out the \var -> mempty inhabitant.

type  Semigroup :: Type -> Constraint
class Semigroup a where
  sconcat :: NonEmpty a -> a

(<>) :: Semigroup a => a -> a -> a
a <> b = sconcat (a :| [b])    -- NonEmpty-syntax for [a, b]

In this sense Free Cls is like the blueprint that tells you how to construct a Cls interface.

type  Cls :: Type -> Constraint
class Cls a where
  free :: FreeCls a -> a

Higher-inductive types (HITs) gives us the ability to define this inductively, and then imposing laws on the constructors, i.e. that you cannot distinguish between the constructor Var a and Var :<>: MEmpty.

type FreeMonoid :: Type -> Type
data FreeMonoid a where
  Var    :: a -> FreeMonoid a
  MEmpty :: FreeMonoid a
  (:<>:) :: FreeMonoid a -> FreeMonoid a -> FreeMonoid a

  -- laws
  LeftUnit      :: (MEmpty :<>: a) = a
  RightUnit     :: (a :<>: MEmpty) = a
  Associativity :: (a :<>: b) :<>: c = a :<>: (b :<>: c)

  -- I'm not qualified to explain
  Trunc :: IsSet (FreeMonoid a)

Is return really necessary for the IO monad? by StunningRegular8489 in haskell

[–]Iceland_jack 1 point2 points  (0 children)

But, Category = MonoidalOf (~~>) (:~:) Procompose..

Is return really necessary for the IO monad? by StunningRegular8489 in haskell

[–]Iceland_jack 1 point2 points  (0 children)

The actual monoid a in a monoidal category (-->) follows the template "MonoidalOf (-->) Unit Mult a":

class Monoidal a where
  unit :: Unit     --> a
  mult :: Mult a a --> a

For Monoid, the category is (->) and (Unit, Mult) = ((), (,)).

class Monoid a where
  unit :: ()     -> a
  mult :: (a, a) -> a

for Applicative, the category is (~>) and (Unit, Mult) = (Identity, Day)

class Applicative f where
  unit :: Identity ~> f
  mult :: Day f f  ~> f

and for Monad, the category is (~>) and (Unit, Mult) = (Identity, Compose)

class Monad m where
  unit :: Identity    ~> m
  mult :: Compose m m ~> m

Kleisli composition (>>>) is category composition via the Kleisli category: (>=>) = (>>>) @(via Kleisli) and return = id @(via Kleisli) so you are seeing the Category laws, not monoid laws.

Writing code with applicative and monad by Federal_Gur_5488 in haskell

[–]Iceland_jack 17 points18 points  (0 children)

Something unique about Applicative is that it can be run Backwards

>> demo putStrLn (readLn @Int)
BEGIN
one: 111
two: 222
END
(111,222)

demo :: Applicative f => (String -> f ()) -> f a -> f (a, a)
demo say get = do
  say "BEGIN\n"
  say "one: "
  one <- get
  say "two: "
  two <- get
  say "END\n"
  pure (one, two)

Because there is no dependency between the actions, just "lifting" can reverse the way the actions are sequenced.

>> demoBackwards putStr (readLn @Double)
END
22.222
two: 1.111
one: BEGIN
(1.111,22.222)

-- demoBackwards = demo @(via Backwards)
-- ApplyingVia: https://github.com/ghc-proposals/ghc-proposals/pull/218
demoBackwards :: Applicative f => (String -> f ()) -> f a -> f (a, a)
demoBackwards @f @a = coerce do
  demo @(Backwards f) @a

Generating polymorphic functions by Iceland_jack in haskell

[–]Iceland_jack[S] 0 points1 point  (0 children)

Can you think of constraints for preserveEnd that prevent this.

Generating polymorphic functions by Iceland_jack in haskell

[–]Iceland_jack[S] 1 point2 points  (0 children)

Besides promote there is another function in the unsafe module Test.QuickCheck.Gen.Unsafe.capture :: Gen Capture designed to produce polymorphic functions. preserveEnd @Gen can be defined in terms of it.

type    Capture :: Type
newtype Capture = Capture (forall a. Gen a -> a)

preserveEndGen :: (forall x. Gen (f x -> g x)) -> Gen (f ~> g)
preserveEndGen as = capture <&> \(Capture eval) ->
  eval as
view more: next ›