descargar - haskell platform windows download

¿Hay una manera de definir un newtype cuantificado existencialmente en GHC Haskell?

Question

¿Es posible en (GHC) Haskell definir un tipo de letra cuantificado existencialmente? Entiendo que si hay clases de tipo involucradas, no se puede hacer en una implementación de paso de diccionario, pero para mis propósitos no se necesitan clases de tipo. Lo que realmente me gustaría definir es esto:

newtype Key t where Key :: t a -> Key t

Pero a GHC no parece gustarle. Actualmente estoy usando data Key t where Key :: !(ta) -> Key t . ¿Hay alguna forma (quizás solo de usar -funbox-strict-fields ?) Para definir un tipo con la misma semántica y sobrecarga que la versión newtype anterior? Tengo entendido que incluso con campos estrictos sin caja, todavía habrá una etiqueta adicional, aunque podría estar totalmente equivocado allí.

Esto no es algo que me esté causando problemas de rendimiento notables. Simplemente me sorprendió que el newtype no estuviera permitido. Soy una persona naturalmente curiosa, por lo que no puedo evitar preguntarme si la versión que tengo se está compilando para la misma representación o si se podría definir cualquier tipo equivalente.

Answer 1

No veo ninguna razón por la que no pueda funcionar, pero quizás ghc tenga algunos problemas de representación interna.

Answer 2

No, según GHC:

Un constructor newtype no puede tener un contexto existencial

Sin embargo, los data están bien:

{-# LANGUAGE ExistentialQuantification #-}
data E = forall a. Show a => E a
test = [ E "foo"
, E (7 :: Int)
, E ''x''
]
main = mapM_ (/(E e) -> print e) test

P.ej

*Main> main
"foo"
7
''x''

Lógicamente, necesitas el diccionario (o etiqueta) asignado en algún lugar. Y eso no tiene sentido si borras el constructor.

Nota : Sin embargo, no puede desempaquetar funciones, como parece indicar, ni campos polimórficos.

¿Hay alguna forma (quizás solo de usar -funbox-strict-fields ?) Para definir un tipo con la misma semántica y sobrecarga que la versión newtype anterior?

Eliminar los -XGADTs me ayuda a pensar sobre esto:

{-# LANGUAGE ExistentialQuantification #-}
data Key t = forall a. Key !(t a)

Como en, Key (Just ''x'') :: Key Maybe

Así que quieres garantizar que el constructor de la Key se borre.

Aquí está el código en GHC para el tipo que verifica las restricciones en newtype :

-- Checks for the data constructor of a newtype
checkNewDataCon con
= do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
-- One argument
; checkTc (null eq_spec) (newtypePredError con)
-- Return type is (T a b c)
; checkTc (null ex_tvs && null eq_theta && null dict_theta) (newtypeExError con)
-- No existentials
; checkTc (not (any isBanged (dataConStrictMarks con)))
(newtypeStrictError con)
-- No strictness

¡Podemos ver por qué ! No tendrá ningún efecto en la representación, ya que contiene componentes polimórficos, por lo que debe utilizar la representación universal. Y el nuevo newtype sin sentido no tiene sentido, ni los constructores no singleton.

Lo único en lo que puedo pensar es que, como newtype los newtype de registros para existenciales, la variable de tipo opaco se escapará si se expone el newtype .