types de données existentielles avec un seul champ strict

Question

J'ai donc un type de données existentielle avec un seul champ strict:

data Uncurry (a :: i -> j -> *) (z :: (i,j)) = 
    forall x y. z ~ '(x,y) => Uncurry !(a x y) 

Expérimentation en utilisant unsafeSizeof (volé this answer) me conduit à croire qu'il peut être nul mémoire- frais généraux:

λ p = (0, '\0') :: (Int, Char) 
λ q = Uncurry p 
λ unsafeSizeof p 
10 
λ unsafeSizeof q 
10 

il semble donc que Uncurry est agissent comme une sorte de newtype, utilisés uniquement au moment de la compilation.

Cela a du sens pour moi, car l'assertion d'égalité ne nécessite pas de charrier de dictionnaire.

Est-ce une interprétation valide? Est-ce que j'ai des garanties de la part de GHC (ou du rapport Haskell), ou est-ce que j'ai eu de la chance?

Answer 1

data n'est jamais transformé en newtype. Uncurry ajoute une nouvelle fermeture, et un pointeur pour le dictionnaire ~ est en fait également transporté, à partir de GHC 8.0.2. Par conséquent, Uncurry a une fermeture avec trois mots.

unsafeSizeof est incorrecte, car Array# stocke sa taille en mots, alors que ByteArray# stocke sa taille en octets, de sorte sizeofByteArray# (unsafeCoerce# ptrs) retourne le nombre de mots plutôt que le nombre prévu d'octets. Une version correcte ressemblerait à ceci sur les systèmes 64 bits:

unsafeSizeof :: a -> Int 
unsafeSizeof !a = 
    case unpackClosure# a of 
    (# x, ptrs, nptrs #) -> 
     I# (8# +# sizeofArray# prts *# 8# +# sizeofByteArray# nptrs) 

Mais notez que unsafeSizeof ne nous donne la taille de la fermeture supérieure. Ainsi, la taille de fermeture de n'importe quel tuple en boîte sera 24, ce qui coïncide avec la taille de fermeture de Uncurry t, puisque Uncurry a un pointeur d'information, un pointeur inutile pour ~, et un pointeur pour le champ de tuple. Cette coïncidence est également valable avec la précédente implémentation buggy unsafeSizeof. Mais la taille totale de Uncurry t est supérieure à celle de t.

Answer 2

Édité pour corriger certains détails re: quads étant 8 octets et expliquant le champ lien statique.

Je pense unsafeSizeOf est inexacte et vous interprétez mal sa sortie. Notez qu'il est destiné à montrer l'utilisation de la mémoire pour la fermeture de niveau supérieur seulement, pas l'utilisation totale de l'espace de l'objet. Qu'est-ce que vous voyez, je pense, est que q nécessite 10 octets plus au tuple p (alors que p nécessite 10 octets plus au Int boxed Char et mis en boîte). De plus, mes tests indiquent que les constructeurs de niveau supérieur ont besoin de 24 octets chacun (sur une architecture 64 bits), même si unsafeSizeOf rapporte 10 pour moi aussi.

si je compile, en particulier, le programme de test suivant avec stack ghc -- -fforce-recomp -ddump-asm -dsuppress-all -O2 ZeroMemory.hs en utilisant GHC 8.0.2:

{-# LANGUAGE ExistentialQuantification #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeFamilies #-} 

module ZeroMemory where 

data Uncurry (a :: i -> j -> *) (z :: (i, j)) = 
    forall x y . z ~ '(x,y) => Uncurry !(a x y) 

q :: Uncurry (,) '(Int, Char) 
q = Uncurry (0, '\0') 

r :: Uncurry (,) '(Int, Char) 
r = Uncurry (1, '\1') 

puis la fermeture empreinte mémoire pour le haut niveau q ressemble:

q_closure: 
    .quad Uncurry_static_info 
    .quad $s$WUncurry_$d~~_closure+1 
    .quad q1_closure+1 
    .quad 3 

Notez que chaque .quad est actuellement 8 octets; c'est un "quad" de "mots" 16 bits à l'ancienne. Je crois que le dernier quad ici, avec la valeur 3, est le "champ de lien statique" décrit dans the GHC implementation commentary et ne s'applique donc pas aux objets d'allocation de tas "typiques".

Ainsi, en ignorant ce dernier champ, la taille totale du niveau supérieur de fermeture q est de 24 octets, et il se réfère à la q1_closure qui représente le tuple contenait:

q1_closure: 
    .quad (,)_static_info 
    .quad q3_closure+1 
    .quad q2_closure+1 
    .quad 3 

pendant 24 octets.

q2 Les

et q3 fermetures sont les encadrés Int et Char et ainsi prendre deux quartes (16 octets) chacune. Donc, q prend un total de 10 quads, ou 80 octets. (J'ai inclus r comme vérification de santé mentale pour m'assurer que je n'identifiais pas les informations partagées.

Un tuple de p aurait à lui seul une empreinte mémoire équivalente à q1_closure, soit 7 quads ou 56 octets.