Emulating OCaml modules with typeclasses

Learn
1

Hey folks!

After reading Deconstructing Classes, I tried to use the idea to mimic a simple OCaml module functor. I have no OCaml knowledge, but basically I want to implement this:

module type STACK = sig
  type 'a t
  val empty : 'a t
  val push  : 'a -> 'a t -> 'a t
end

module ListStack : STACK = struct
  type 'a t = 'a list
  let empty = []
  let push x s = x :: s
end

module MakeSized (S : STACK) : sig
  include STACK with type 'a t = 'a S.t
  val size : 'a t -> int
end = struct
  include S
  let size s = List.length s     (* Don't mind this one... as it relies on S.t being list-based *)
end

I have this now in Haskell:

{-# LANGUAGE DerivingStrategies, TypeFamilies, AllowAmbiguousTypes #-}

import Data.Kind

class Stack (m :: k) where
  type Elem m :: Type

  type Container m :: Type -> Type

  empty :: Container m (Elem m)
  push :: (Elem m) -> (Container m (Elem m)) -> (Container m (Elem m))

data ListStack (a :: Type)

instance Stack (ListStack a) where
  type Elem (ListStack a) = a
  type Container (ListStack a) = []

  empty :: [a]
  empty = []

  push :: a -> [a] -> [a]
  push = (:)

class (Stack m) => SizedStack (m :: k) where
  size :: Container m (Elem m) -> Int

instance SizedStack (ListStack a) where
  size :: [a] -> Int
  size = length

So far, so good. But the issue is I can’t seem to find any way to actually “use” this concoction; I used AllowAmbiguousTypes so that I can use TypeApplications to disambiguate it. But:

stack :: [Int]
stack = empty @(ListStack Int)

Gives:

• Couldn't match type ‘Elem m0’ with ‘Int’
  Expected: [Int]
    Actual: Container m0 (Elem m0)
  The type variable ‘m0’ is ambiguous
• In the expression: empty @(ListStack Int)
  In an equation for ‘stack’: stack = empty @(ListStack Int) typecheck(GHC-83865)

And this:

stack :: forall m. (m ~ ListStack Int, Stack m) => Container m (Elem m)
stack = empty @m

Gives:

• Could not deduce ‘Stack m0’ arising from a use of ‘empty’
  from the context: (m1 ~ ListStack Int, Stack m1)
    bound by the type signature for:
               stack :: forall m1.
                        (m1 ~ ListStack Int, Stack m1) =>
                        Container m1 (Elem m1)
    at C:\Users\saeid\Projects\Haskell\playground\src\Scratch.hs:54:1-71
  The type variable ‘m0’ is ambiguous
  Relevant bindings include
    stack :: Container m1 (Elem m1)
• In the expression: empty @m
  In an equation for ‘stack’: stack = empty @m typecheck(GHC-39999)
• Couldn't match type ‘Elem m0’ with ‘Int’
  Expected: Container m1 (Elem m1)
    Actual: Container m0 (Elem m0)
  The type variable ‘m0’ is ambiguous
• In the expression: empty @m
  In an equation for ‘stack’: stack = empty @m
• Relevant bindings include
    stack :: Container m1 (Elem m1)
      typecheck(GHC-83865)
empty :: forall k (m :: k). Stack m => Container m (Elem m)

Is there a way to make the type checker happy using the class definitions as is, or refactor the types somehow to make it work? Or is it plain impossible?

Any hints or ideas would be greatly appreciated!

2

The problem is that Stack is kind-polymorphic, so the type of empty is:

ghci> :t empty
empty :: forall k (m :: k). Stack m => Container m (Elem m)

So you need to invoke it like this: empty @_ @(ListStack Int)

Alternatively, you can make Stack and SizedStack not kind-polymorphic by replacing k with Type. I don’t see any reason not to do that.

2 Likes
3

You may find this interesting: modules-for-lennart

1 Like