Hiding type variables from the signature?
Hello café, hope you all doing well! I have this code [1]. Its purpose is to provide an `fmap` that works at any depth. Here is the gist of the gist: ```Haskell fmapz ∷ forall seed fruit seed' fruit' peels recursive. Squeezish seed seed' fruit fruit' peels recursive ⇒ (seed → seed') → fruit → fruit' fmapz function = stretch . fmap @(Squeezed (Strip seed fruit)) function . squeeze ``` As the examples show, it works, and even has some type inference. However, the type signature is unwieldy. It seems like it should have only 4 variables, but I have to also do some type level book-keeping for which the other 2 variables are needed. These book-keeping type variables are determined by type families from the other 4, so surely I can hide them inside a type synonym or something like that? I tried giving a quantified constraint, like so: ```Haskell type Squeezish ∷ ★ → ★ → ★ → ★ → Constraint type Squeezish seed seed' fruit fruit' = forall peels recursive. Squeezish' seed seed' fruit fruit' peels recursive class Squeezish' seed seed' fruit fruit' (peels ∷ [★ → ★]) (recursive ∷ Bool) instance ( peels ~ Strip seed fruit , ForAll peels Functor , Squeezy seed' fruit' peels recursive , Squeezy seed fruit peels recursive ) ⇒ Squeezish' seed seed' fruit fruit' peels recursive ``` — But then the constraints from the context of `Squeezish'` fail to make it to the use site and numerous errors arise. What can I do to solve this problem? Or is it theoretically impossible? [1]: https://gist.github.com/kindaro/6056f753bcf356ced96b817fee72533c
Alright, I managed to circumvent this problem by adding more type classes with functional dependencies. Problematic version, for reference: https://gist.github.com/kindaro/6056f753bcf356ced96b817fee72533c/335e4399f50... Current version: https://gist.github.com/kindaro/6056f753bcf356ced96b817fee72533c/b556f85589a... ```Haskell fmapz :: forall peels seed seed'. Functors seed seed' peels => (seed -> seed') -> Dress seed peels -> Dress seed' peels fmapz function = stretch . fmap @(Squeezed peels) function . squeeze ``` — Much more better!
Alright, I found a nice example of how things fail. See this addition to the previous code: ```Haskell -- | This is the right tensorial strength of a functor with respect to tupling. deasil :: Functor functor => (functor left, right) -> functor (left, right) deasil (functor, value) = fmap (, value) functor deasilsA :: forall peels seed value. ( Squeezy seed (Dress seed peels) peels , ForAll peels Functor ) => (Dress seed peels, value) -> Squeezed peels (seed, value) deasilsA = deasil . first squeeze deasilsB :: forall peels seed value. ( Squeezy (seed , value) (Dress (seed, value) peels) peels ) => Squeezed peels (seed, value) -> Dress (seed, value) peels deasilsB = stretch deasils :: _ => (Dress seed peels, value) -> Dress (seed, value) peels deasils = deasilsB . deasilsA ``` What is the type of `deasils`? ``` % ghci-9.2.2 Squeeze.hs GHCi, version 9.2.2: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/kindaro/code/dotfiles/ghci.conf [1 of 1] Compiling Main ( Squeeze.hs, interpreted ) Ok, one module loaded. λ :type deasilsB . deasilsA deasilsB . deasilsA :: (ForAll peels Functor, Squeezy' seed (Dress seed peels) peels (Strip seed (Dress seed peels) == '[]), Squeezy' (seed, value) (Dress (seed, value) peels) peels (Strip (seed, value) (Dress (seed, value) peels) == '[])) => (Dress seed peels, value) -> Dress (seed, value) peels ``` Looks good, but… ``` λ f = deasilsB . deasilsA <interactive>:2:1: error: • Could not deduce: Dress seed0 peels0 ~ Dress seed peels ``` What is going on? How can I have my `deasils`? I tried attaching all kinds of type annotations, but nothing works so far. I do not even understand the problem. How is it that an expression can be typed, but cannot be assigned to a name? You can see the complete code at the gist [1]. [1]: https://gist.github.com/kindaro/6056f753bcf356ced96b817fee72533c/2823ec2792f...
participants (1)
-
Ignat Insarov