The ConstraintKinds extension just lets you deal with kinds involving constraints. Turn it on, import the Constraint kind from somewhere (I know it's exported from GHC.Exts and also from Data.Constraint in the constraints package; I don't know if it has a nice home in base). Then you can write things like

class C f a where
  p :: f a => proxy f -> a -> Int

etc.

On Jan 23, 2017 4:19 PM, "Olaf Klinke" <olf@aatal-apotheke.de> wrote:
On a mostly unrelated note, Dan Doel elaborated [1] that the list monad is not the monad of free monoids either, even though mathematically the free monoid over x is the set of words of finite length with alphabet x. Briefly, the reason is that Haskell types are domains, not sets.

Below is a proof that the free monad is not the free algebra.

One approximant to free algebraic structures is to look at the free F-algebra for a functor F. This approach does not take into account any equations between the algebraic operations.

{-# LANGUAGE Rank2Types,MultiParamTypeClasses,FlexibleInstances,FlexibleContexts #-}
module FreeFAlg where
import Control.Applicative
import Control.Monad

-- F-algebras (sans laws).
class Functor f => Alg f a where
    alg :: f a -> a

-- The free F-algebra over x, following Dan Doel's ideas,
-- with the universal property baked in.
newtype FreeAlg f x = FreeAlg (forall a. Alg f a => (x -> a) -> a)
runFree :: Alg f a => FreeAlg f x -> (x -> a) -> a
runFree (FreeAlg f) = f
universal :: Alg f a => (x -> a) -> FreeAlg f x -> a
universal = flip runFree
instance Functor f => Alg f (FreeAlg f x) where
    alg ff = FreeAlg (\f -> alg (fmap (($f).runFree) ff))
instance Functor (FreeAlg f) where
    fmap h (FreeAlg fx) = FreeAlg (\f -> fx (f.h))
instance Monad (FreeAlg f) where
    return x = FreeAlg ($x)
    (FreeAlg fx) >>= k = FreeAlg (\f -> fx (\x -> runFree (k x) f))
instance Applicative (FreeAlg f) where
    pure = return
    (<*>) = ap

data FreeMonad f x = Pure x | Roll (f (FreeMonad f x))
instance Functor f => Alg f (FreeMonad f x) where
    alg = Roll

-- This looks like the same universal property...
universal' :: Alg f a => (x -> a) -> FreeMonad f x -> a
universal' f (Pure x) = f x
universal' f (Roll ffree) = alg  (fmap (universal' f) ffree)

freeAlg2freeMonad :: Functor f => FreeAlg f x -> FreeMonad f x
freeAlg2freeMonad = universal Pure
freeMonad2freeAlg :: Functor f => FreeMonad f x -> FreeAlg f x
freeMonad2freeAlg = universal' return

The free monad is not the free F-algebra, because uniqueness fails.
Consider the constant functor

data Point a = Point
instance Functor Point where
    fmap f Point = Point
-- universal' f (Pure x) = f x
-- universal' f (Roll Point) = alg Point
-- but we have another function with the same type as universal':
notUnique :: Alg Point a => (x -> a) -> FreeMonad Point x -> a
notUnique f = const (alg Point)

For classes like Monoid, which have equations between the algebraic operations (such as mappend mempty = id), we'd need the language extension that allows constraints as type parameters. I'd like to write

Free Monoid x = Free (forall a. Monid a => (x -> a) -> a)

but I am not experienced with the ConstraintKinds extension. Anyone help?

Olaf

[1] http://comonad.com/reader/2015/free-monoids-in-haskell/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.