Existential data types with one strict field

So, I have an existential data type with a single strict field:

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

Experimenting using unsafeSizeof (stolen from this answer ) makes me think that this could be zero memory:

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

So, it looks like Uncurry is kind of like a newtype , which is used only at compile time.

This makes sense to me, since the statement of equality does not require translation of the dictionary.

Is this a valid interpretation? Do I have any guarantees from the GHC (or the Haskell report), or am I just lucky?

+5
source share
2 answers

data never converted to newtype . Uncurry adds a new closure, and the pointer for the dictionary ~ actually also moves around the map with GHC 8.0.2. Therefore, Uncurry has a three-word closure.

unsafeSizeof incorrect because Array# saves its size in words, and ByteArray# saves its size in bytes, so sizeofByteArray# (unsafeCoerce# ptrs) returns the number of words, not the specified number of bytes. The correct version will look approximately on 64-bit systems:

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

But note that unsafeSizeof gives us the size of the topmost closure. Thus, the closure size of any insertion tuple will be 24 , which is the same as the closure size of Uncurry t , since Uncurry has an information pointer, a useless pointer for ~ and a pointer to the tuple field. This match also occurs with the previous unsafeSizeof error. But the overall size of Uncurry t larger than that of t .

+6
source

Edited to correct some of the details of re: quads, consisting of 8 bytes and explaining the static link field.

I think unsafeSizeOf is inaccurate and you are misinterpreting its output. Please note that it is intended to display memory usage only for closing the top level, and not for general use of the object space. What you see, I think, is that q requires 10 bytes in addition to the tuple p (while p requires 10 bytes in addition to the Char box and in the Int box). Moreover, my tests show that top-level constructors actually require 24 bytes each (in a 64-bit architecture), although unsafeSizeOf reports 10 for me too.

In particular, if I compile the following test program using stack ghc -- -fforce-recomp -ddump-asm -dsuppress-all -O2 ZeroMemory.hs using GHC 8.0.2:

 {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} module ZeroMemory where data Uncurry (a :: i -> j -> *) (z :: (i, j)) = forall xy . z ~ '(x,y) => Uncurry !(axy) q :: Uncurry (,) '(Int, Char) q = Uncurry (0, '\0') r :: Uncurry (,) '(Int, Char) r = Uncurry (1, '\1') 

then the memory size for closing the top level q as follows:

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

Note that each .quad here is actually 8 bytes; it is a “quad” of 16-bit “old words” of the old style. I believe that the final quad here with a value of 3 is the "static link field" described in the commentary on the GHC implementation and, t apply to the "typical" heap distribution objects.

Thus, ignoring this final field, the total closing size of the top level q is 24 bytes, and it refers to q1_closure , which is the contained tuple:

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

for another 24 bytes.

The closures q2 and q3 are plug-in Int and Char and therefore occupy two squares (16 bytes each). So q takes up a total of 10 quads or 80 bytes. (I included r as a health check to make sure that I did not mistakenly identify any general information.)

A p tuple itself will have a memory size equivalent to q1_closure , so 7 quads or 56 bytes.

+5
source

Source: https://habr.com/ru/post/1271939/


All Articles