|
Hello everyone,
I am currently working on a Haskell fuzzer and new to Racket and Xsmith in general, so I apologize in advance if this question is trivial. There is something I don't understand about the types in Xsmith: I emulate Haskell's numerical types like this:
(define number-type (base-type 'number #:leaf? #f)) (define real-type (base-type 'real number-type #:leaf? #f))
(define integral-type (base-type 'integral real-type #:leaf? #f))
(define int-type (base-type 'int integral-type))
(define integer-type (base-type 'integer integral-type))
(define fractional-type (base-type 'fractional real-type #:leaf? #f))
(define float-type (base-type 'float fractional-type))
I then define the type info from the Minus _expression_ like this: (define numeric-bin-op-subtype (λ (n t) (hash 'l t 'r t)))
[Minus [(fresh-subtype-of number-type) numeric-bin-op-subtype]]
My assumption was that both Minus children nodes would be constrained to all the non-leaf nodes in either integral-type, or fractional-type. However, Xsmith still generates Minus nodes with 'l integral and 'r fractional, causing a type constraint violation in Haskell. I have since switched to using (fresh-type-variable integral-type fractional-type). This works, but I am still puzzled about fresh-subtypes. REPL experiments confirm that even fresh-subtypes of my real-types can be unified with both fractional-type and integral-type. What happens when a fresh-subtype is created? Regards, Everard de Vree |