Changes between Initial Version and Version 1 of Ticket #5855


Ignore:
Timestamp:
Feb 10, 2012 11:01:13 AM (2 years ago)
Author:
simonpj
Comment:

(I've added some type signatures.)

Can you explain why you think the program should not diverge? That is, why is this a bug?

Changing compose to use lazy pattern matching makes it converge:

compose ~(PHom f1 g1) ~(PHom f2 g2) = PHom (f2 . f1) (g2 . g1)

Simon

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #5855

    • Property Difficulty changed from to Unknown
  • Ticket #5855 – Description

    initial v1  
    1313>   FSucc2 :: p Fst -> FNat p Snd 
    1414 
     15> hmap :: PHom t p -> PHom (FNat t) (FNat p) 
    1516> hmap (PHom f g) = PHom hf hg where 
    1617>   hf FZero = FZero 
     
    2829>   g (Succ2 n) = FSucc2 n 
    2930 
     31> compose :: PHom p1 t -> PHom t p2 -> PHom p1 p2 
    3032> compose (PHom f1 g1) (PHom f2 g2) = PHom (f2 . f1) (g2 . g1) 
    3133 
     34> fold :: PHom (FNat p) p -> PHom Nat p 
    3235> fold phi = compose out (compose (hmap (fold phi)) phi)  
    3336