Closed joshrule closed 5 years ago
Yeah, this is because the program you gave isn’t well typed (yikes that error message could use improvement). The type of the routine input is based on its first usage in a subroutine, it doesn’t propagate dependent type constraints backwards. In this case, tail
takes an int-list with length at least 1 and its return type is a list with length one fewer than the input. Hence generated inputs will be lists of length at least one. However, head
has the same constraint on its input, but that means we need a list with length two for the program to type.
Maybe you could try adding a subroutine to serve as a precondition, like take-list-length-at-least-two → tail → head. Could also try getting the type constraints to flow back up the subroutines, but I think that’s difficult
Thanks—now I know!
For very simple routines,
./lr_cli
appears to work just fine:But, even simple modifications tend to fail:
Any ideas as to what's happening here?