haskell - newtype con RankNTypes

higher-rank-types

Question

Si quiero declarar un newtype tal que el tipo de tipo del valor está restringido para tener una instancia para una clase de tipo, parece que puedo hacerlo con:

{-# LANGUAGE RankNTypes #-}

newtype ShowBox = ShowBox (forall a. Show a => a)

GHC compila eso bien, pero cuando lo intento y uso ShowBox con

ShowBox "hello"

Me sale un error de compilación

<interactive>:1:18:
    Could not deduce (a ~ [Char])
    from the context (Show a)
      bound by a type expected by the context: Show a => a
      at <interactive>:1:10-24
      `a'' is a rigid type variable bound by
          a type expected by the context: Show a => a at <interactive>:1:10
    In the first argument of `ShowBox'', namely `"hello"''
    In the expression: ShowBox "hello"
    In an equation for `a'': a = ShowBox "hello"

¿Hay alguna manera de hacer que esto funcione?

Answer 1

Bueno, tu constructor de Show tiene este tipo:

Show :: (forall a. Show a => a) -> ShowBox

Está intentando aplicar esta función al tipo [Char] , que no es del tipo forall a. Show a => a forall a. Show a => a , porque a es una "variable de Skolem" que solo se puede unificar con otro tipo bajo reglas muy estrictas (que otros podrán explicar mejor que yo).

¿Está seguro de que lo siguiente no es lo que quiere ( data módulo vs. newtype )? ¿Por qué forall al forall dentro del constructor?

-- Show :: Show a => a -> ShowBox
data ShowBox = forall a. Show a => Show a

Answer 2

Le está prometiendo al compilador que el valor que ponga dentro de un ShowBox tendrá el tipo para todos forall a. Show a => a forall a. Show a => a . Solo hay un valor posible con ese tipo, y es _|_ . Creo que probablemente quieras un tipo existencial, que parece bastante similar, pero significa algo muy diferente.

{-# LANGUAGE ExistentialQuantification #-}

data ShowBox = forall a. Show a => ShowBox a

Esto debe hacerse con data , en lugar de newtype . La coincidencia de patrones en el constructor es lo que lleva la instancia de Show al ámbito, en este caso. Dado que los newtype no tienen representación en tiempo de ejecución, no tienen lugar para almacenar el testigo polimórfico que implica la cuantificación existencial.