weixin_39639260
weixin_39639260
2021-01-02 12:08

Add sumToTag# primop (under review)

Add a sumToTag# primop for extracting the numerical value of an alternative of an unboxed sum type.

Rendered proposal

该提问来源于开源项目:ghc-proposals/ghc-proposals

  • 点赞
  • 写回答
  • 关注问题
  • 收藏
  • 复制链接分享
  • 邀请回答

21条回答

  • weixin_39639260 weixin_39639260 4月前

    , as a week has gone by with no comments, I submit this proposal to the committee.

    点赞 评论 复制链接分享
  • weixin_39639260 weixin_39639260 4月前

    , will you please assign a shepherd?

    点赞 评论 复制链接分享
  • weixin_39960116 weixin_39960116 4月前

    Ups, sorry, this must have slipped through my radar, thanks for the nudge.

    点赞 评论 复制链接分享
  • weixin_39753211 weixin_39753211 4月前

    in the change specification section, can you specify the precise type of sumToTag#?

    点赞 评论 复制链接分享
  • weixin_39639260 weixin_39639260 4月前

    in the change specification section, can you specify the precise type of sumToTag#?

    Like dataToTag#, it's impossible to give it a precise type in Haskell. The best we can do is

    haskell
    sumToTag# :: forall xs (a :: TYPE ('SumRep xs)). a -> Int#
    

    But the forall is a lie—xs must be fully determined at compile time.

    点赞 评论 复制链接分享
  • weixin_39753211 weixin_39753211 4月前

    This reminds me of #17201 on Gitlab. I don't think there is anything wrong with dataToTag#, actually, maybe you're speaking of tagToEnum# (whose specification I'm not sure of)?

    Nevertheless, the specification section should not leave the reader guessing as to what, precisely, you are proposing.

    点赞 评论 复制链接分享
  • weixin_39639260 weixin_39639260 4月前

    This reminds me of #17201 on Gitlab. I don't think there is anything wrong with dataToTag#, actually, maybe you're speaking of tagToEnum# (whose specification I'm not sure of)?

    Nevertheless, the specification section should not leave the reader guessing as to what, precisely, you are proposing.

    This reminds me of #17201 on Gitlab. I don't think there is anything wrong with dataToTag#, actually, maybe you're speaking of tagToEnum# (whose specification I'm not sure of)?

    Nevertheless, the specification section should not leave the reader guessing as to what, precisely, you are proposing.

    Unfortunately, I don't understand this comment. Could you expand? How does it relate to that GitHub issue? What aspect of the proposal don't you understand? Yes, I think I did mix up an aspect of dataToTag# with one of tagToEnum#. The proposed primop would have type checking requirements analogous to tagToEnum#. I will edit the proposal to reflect that.

    点赞 评论 复制链接分享
  • weixin_39753211 weixin_39753211 4月前

    Unfortunately, I don't understand this comment. Could you expand? How does it relate to that GitHub issue?

    Sure. In the Gitlab issue link, the discussion veers towards creating a new kind of constraint FixedRuntimeRep :: RuntimRep -> Constraint, whose role is precisely to ensure that a runtime representation argument is fully determined. It's a similar constraint to what you would need to give a precise type to sumToTag# if I understand correctly.

    点赞 评论 复制链接分享
  • weixin_39639260 weixin_39639260 4月前

    , I hope the commit I pushed addresses your concerns.

    点赞 评论 复制链接分享
  • weixin_39887577 weixin_39887577 4月前

    Thanks for the updates .

    -proposals/ghc-steering-committee I recommend accepting this proposal. It's a simple addition that fills a gap in the API for unboxed sums (we already have dataToTag# for lifted types).

    The Unresolved Questions section discusses a possible tagToSum# function analogous to tagToEnum#. For the same reasons mentioned in the proposal, I recommend we do not implement tagToSum# at this time.

    点赞 评论 复制链接分享
  • weixin_39774445 weixin_39774445 4月前

    The forall feels like a bit of a lie: much like tagToEnum# can be compiled only when..

    I think you mean dataToTag#.

    the type constructor of its argument is known and is an algebraic datatype, sumToTag# can be compiled only when the runtime representation of its argument is known and is 'SumRep xs for some known xs.

    What does "known" mean? I think you mean, more precisely * the first (type) argument to sumToTag# must be closed (i.e. have no free variables)

    So (after type inference is complete) you can have * sumToTag# @[IntRep] or * sumToTag# @[IntRep, IntRep, PtrRep], * sumToTag# @[IntRep, TupleRep[PtrRep,PtrRep]] but NOT * sumToTag#, or * sumToTag# @[r,IntRep]

    This restriction doesn't actually have any effect in practice, because bindings can't be representation-polymorphic anyway.

    I'm really not sure what this means. You could say sumToTag# (error "urk"), where r is some in-scope type variable.

    点赞 评论 复制链接分享
  • weixin_39774445 weixin_39774445 4月前

    I'm ok with this proposal, modulo the clarifications above.

    点赞 评论 复制链接分享
  • weixin_39774445 weixin_39774445 4月前

    Note: the choice to make the first alternative 1# rather than 0# is poorly motivated, and should probably be changed, but that's beyond the strict scope of this proposal.

    I think it's because data constructor tags start at 1; we use 0 for "thunk".

    点赞 评论 复制链接分享
  • weixin_39639260 weixin_39639260 4月前

    The forall feels like a bit of a lie: much like tagToEnum# can be compiled only when..

    I think you mean dataToTag#.

    No, dataToTag# isn't at all fussy, is it? But we need to know the result type to compile tagToEnum#.

    the type constructor of its argument is known and is an algebraic datatype, sumToTag# can be compiled only when the runtime representation of its argument is known and is 'SumRep xs for some known xs.

    What does "known" mean? I think you mean, more precisely

    • the first (type) argument to sumToTag# must be closed (i.e. have no free variables)

    That could work.

    So (after type inference is complete) you can have

    • sumToTag# @[IntRep] or
    • sumToTag# @[IntRep, IntRep, PtrRep],
    • sumToTag# @[IntRep, TupleRep[PtrRep,PtrRep]] but NOT
    • sumToTag#, or
    • sumToTag# @[r,IntRep]

    Yes.

    This restriction doesn't actually have any effect in practice, because bindings can't be representation-polymorphic anyway.

    I'm really not sure what this means. You could say sumToTag# (error "urk"), where r is some in-scope type variable.

    Ah, I suppose you could! And that would actually be fine, wouldn't it? So maybe my well-intentioned restriction isn't actually needed at all!

    点赞 评论 复制链接分享
  • weixin_39639260 weixin_39639260 4月前

    Note: the choice to make the first alternative 1# rather than 0# is poorly motivated, and should probably be changed, but that's beyond the strict scope of this proposal.

    I think it's because data constructor tags start at 1; we use 0 for "thunk".

    Yes, I have heard it was by analogy to the way it's done for lifted sums, but we don't have thunks for unboxed sums, so we don't need that. If we make them 0-indexed instead, and work from low to high instead of high to low, I believe we should sometimes be able to drop cmp instructions (probably in peephole optimization). Again, out of scope for the proposal.

    点赞 评论 复制链接分享
  • weixin_39887577 weixin_39887577 4月前

    Note: the choice to make the first alternative 1# rather than 0# is poorly motivated, and should probably be changed, but that's beyond the strict scope of this proposal.

    I think it's because data constructor tags start at 1; we use 0 for "thunk".

    Are the 1-indexed tags exposed via dataToTag#, or do we reindex from 0 since dataToTag# requires its argument to be evaluated? I think consistency between the two APIs would be good.

    点赞 评论 复制链接分享
  • weixin_39639260 weixin_39639260 4月前

    Are the 1-indexed tags exposed via dataToTag#, or do we reindex from 0 since dataToTag# requires its argument to be evaluated? I think consistency between the two APIs would be good.

    No, the 1-indexed tags for lifted types are reindexed to 0 by dataToTag#.

    点赞 评论 复制链接分享
  • weixin_39639260 weixin_39639260 4月前

    Let me be totally clear:

    haskell
    dataToTag# False = 0#
    dataToTag# True = 1#
    

    In the current proposal,

    haskell
    sumToTag (# (##) | #) = 0#
    sumToTag (# | (##) #) = 1#
    

    They are consistent.

    点赞 评论 复制链接分享
  • weixin_39774445 weixin_39774445 4月前

    It looks like GHC already has a blanket restriction on representation-polymorphic arguments. We can't generate code for passing the argument without knowing its representation, so this makes sense.

    Yes exactly. You could refer (in the proposal) to Section 5 of Levity Polymorphism

    点赞 评论 复制链接分享
  • weixin_39753211 weixin_39753211 4月前

    As far as I'm concerned, the suggested edits are good.

    点赞 评论 复制链接分享
  • weixin_39887577 weixin_39887577 4月前

    have you had a chance to look at my suggested edits? I think that's the only thing blocking us from merging this proposal.

    点赞 评论 复制链接分享