Opened 5 years ago

Closed 5 years ago

Last modified 5 years ago

#10048 closed feature request (invalid)

{-# UNPACK #-} support for size-indexed types

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.11
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I don't know too much of the theory, but it seems to me that {-# UNPACK #-} should be able to work for something like this:

data Tup (l::[*]) where
    Nil  :: HList '[]
    Cons :: e -> {-# UNPACK #-} !(HList l) -> HList (e ': l)

This is essentially just HList from the HList package but strict in the second Cons argument. What I would want is for Tup '[a,b,c] to be represented in just the same way as (a,b,c). When possible, I'd want the getters/setters/lenses to be optimized to index into the unpacked structure rather than walking along it.

Change History (3)

comment:1 Changed 5 years ago by rwbarton

How would we implement

hlength :: HList l -> Int
hlength Nil = 0
hlength (Cons _ xs) = 1 + hlength xs

then? (Bear in mind that we have no access to the type parameter l at runtime.)

I think this sort of thing could only work with a type family rather than a GADT (and even then I haven't thought about whether it actually could work).

comment:2 in reply to:  1 Changed 5 years ago by dfeuer

Resolution: invalid
Status: newclosed

Replying to rwbarton:

How would we implement

hlength :: HList l -> Int
hlength Nil = 0
hlength (Cons _ xs) = 1 + hlength xs

then? (Bear in mind that we have no access to the type parameter l at runtime.)

I think this sort of thing could only work with a type family rather than a GADT (and even then I haven't thought about whether it actually could work).

Ah, you make a very good point.

comment:3 Changed 5 years ago by simonpj

A difficulty is that in GHC today, each data constructor (such as Cons above) has a single, fixed memory layout. So if we have

data T = MkT Bool {-# UNPACK !(Int, Int) #-}

we can decide to lay out MkT with a Bool field and two Int fields.

But if we don't know l, we don't know how HList l is represented, so we can't do that.

It's not just an implementation matter. Suppose at an allocation site we were allocating a Cons whose first arg was '[Int,Bool]. Then you could imagine whizzing up a specialised Cons constructor. But then hlength above would have to be able to consume that constructor!

I don't know any way to do this without monomorphising the code. Which is often, but not always possible, so you'd also need an escape hatch for the impossible case -- and it's not obvious how to build the hatch.

PhD thesis anyone?

Simon

Note: See TracTickets for help on using tickets.