Icelandjack

http://www.michaelburge.us/2017/09/27/delta-debugging-in-haskell.html

data HList f xs where
  HNil  :: HList f '[]
  HCons :: f a -> HList f as -> HList f (a ': as)

divideGeneral :: forall f a bs. Divisible f => (a -> HList Identity bs) -> (HList f bs -> f a)
divideGeneral f = \case
  HNil ->

Icelandjack

Getting Num, Floating, Fractional from Applicative

newtype WrappedApplicative f a = WrapApplicative (f a)
  deriving 
    (Functor, Show)
  deriving newtype 
    Applicative

instance (Applicative f, Num a) => Num (WrappedApplicative f a) where

Icelandjack

{-# Language StandaloneDeriving, PatternSynonyms, GADTs, UndecidableInstances, ScopedTypeVariables, TemplateHaskell, TypeInType, TypeOperators, TypeFamilies, AllowAmbiguousTypes, InstanceSigs, TypeApplications #-}

import Data.Singletons
import Data.Singletons.Prelude.Base
import Data.Singletons.TH
import Data.Kind
import Control.Arrow ((***))

data Dup :: Type ~> Type

Icelandjack

Embedding F with a twist.

Icelandjack

• Continued in Explicit Witnesses of Monoid Actions, Semigroup / Monoid / Applicative homomorphisms

Reddit discussion

My initial motivation for -XDerivingVia was deriving across isomorphisms.

Standard type-class encodings of isos turn out to be awkward due to overlap.

Icelandjack

demoteMonoid :: (forall m. Monoid m => m) -> Semigroup m => Maybe m
demoteMonoid k = eval k where
  eval :: MONOID m -> Semigroup m => Maybe m
  eval = getOption . foldMap (Option . Just)

data MONOID a = NIL | SING a | MONOID a :<> MONOID a
  deriving Foldable

instance Monoid (MONOID a) where

Icelandjack

class ListLike f where
  nil  :: f a
  cons :: a -> f a -> f a
  (·)  :: f a -> f a -> f a

newtype LL a = LL (forall ff. ListLike ff => ff a)

instance ListLike LL where
 nil :: LL a

Icelandjack

https://twitter.com/phadej/status/958227051374350336

{-# Language QuantifiedConstraints #-}

class    (forall xx. Eq xx => Eq (f xx)) => Eq1 f
instance (forall xx. Eq xx => Eq (f xx)) => Eq1 f

newtype New s a = New a

Icelandjack

{-# Language QuantifiedConstraints #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language MultiParamTypeClasses #-}
{-# Language UndecidableSuperClasses #-}
{-# Language FlexibleInstances #-}
{-# Language UndecidableInstances #-}
{-# Language AllowAmbiguousTypes #-}

data D c where

Icelandjack

-- Response to
--   https://gist.github.com/sjoerdvisscher/e8ed8ca8f3b6420b4aebe020b9e8e235
--   https://twitter.com/sjoerd_visscher/status/975375241932427265

{-# Language QuantifiedConstraints, TypeOperators, RankNTypes, GADTs, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, InstanceSigs #-}

import Data.Coerce

type f ~> g = forall x. f x -> g x