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!