Recursive contract expanding infinitely?

[dbp]

Just defining this:

(define-contract SExp (OneOf Symbol
                             Integer
                             Boolean
                             (List SExp)))

Works fine (using, as I understand, the stuff you did to autodetect the recursive binding).

But trying to use it:

(: f (-> SExp True))
(define (f s) #t)

Seems to infinite loop (or at least, OOMs..)

[camoy]

I think this is because List is not defined as (OneOf Nil (Cons X (List X)), but rather as a flat contract. For this to work, we might have to define our own lists and replace Racket's built-in ones.

[dbp]

This seems relatively important, as I think Lists will end up being used like this in various places (n-ary trees for example). Not worth special casing the contract for list to not be Flat, is it?

On Wed, Dec 20, 2023, at 11:18 PM, Cameron Moy wrote:

I think this is because List is not defined as (OneOf Nil (Cons X (List X)), but rather as a flat contract. For this to work, we might have to define our own lists and replace Racket's built-in ones.

— Reply to this email directly, view it on GitHub https://github.com/logiccomp/lsl/issues/7#issuecomment-1865453411, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAELBJMRM56Q4ULXRYYB6STYKOZ7XAVCNFSM6AAAAABA5LTLLSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNRVGQ2TGNBRGE. You are receiving this because you authored the thread.Message ID: @.***>

[camoy]

That's another possibility. I can try that solution first and see if it's easier.