I'm having trouble with typed Racket. I have code that works perfectly as "#lang racket", but when I swap that to typed/racket, I get a couple errors, and I haven't been able to convince the typechecker that things will work.
The start is a call to (current-directory), and then I do various bits of processing on that, and various things are complaining about mismatches with the Path, Path-String, and Path-For-Some-System types. The errors I get are:
in-git-repo.rkt:34:24: Type Checker: type mismatch
expected: (U Path-For-Some-System Path-String)
given: Any
in: p
in-git-repo.rkt:34:24
in-git-repo.rkt:48:41: Type Checker: Polymorphic function `first' could not be applied to arguments:
Domains: (Listof a)
(Pairof a (Listof b))
Arguments: (Pairof Any Any)
in: (first path-components)
in-git-repo.rkt:48:41
in-git-repo.rkt:59:6: Type Checker: type mismatch
expected: (U Path-For-Some-System Path-String)
given: Any
in: path
in-git-repo.rkt:59:6
in-git-repo.rkt:79:16: Type Checker: type mismatch
expected: Path
given: Path-For-Some-System
in: (apply build-path _)
in-git-repo.rkt:79:16
Type Checker: Summary: 4 errors encountered
How do I approach fixing this? Somehow, I think, I need to start with coercing between Path and Path-For-Some-System types. Does that sound right?
Here is an excerpt from your code that reproduces the first type error:
#lang typed/racket
;;;(define (path-is-dot-git? [p : (U 'same 'up Path-For-Some-System)])
(define (path-is-dot-git? p)
(path-has-extension? p ".git"))
You have commented out the type annotation, so Typed Racket tries to use the type Any for p. But you pass p to path-has-extension?, which has this type:
> (:print-type path-has-extension?)
(-> (U Path-For-Some-System Path-String) (U Bytes String) (U Bytes False))
The error:
Type Checker: type mismatch
expected: (U Path-For-Some-System Path-String)
given: Any in: p
tells you that p (specifically pointing to the use of p as the first argument to path-has-extension? has the type Any, which doesn't work for the needed type (U Path-For-Some-System Path-String).
Specifying the type of p fixes the error:
#lang typed/racket
(define (path-is-dot-git? [p : Path-String])
(path-has-extension? p ".git"))
Now, path-is-dot-git? has this type:
> (:print-type path-is-dot-git?)
(-> Path-String (U Bytes False))
However, your comment said that you wanted for p to have the type (U 'same 'up Path-For-Some-System) (note that this excludes String!), and you might want the result type to be Boolean. Here's a version that achieves that:
#lang typed/racket
(define (path-is-dot-git? [p : (U 'same 'up Path-For-Some-System)])
(or (equal? p (string->path ".git"))
(and (not (symbol? p))
(path-has-extension? p ".git")
#t)))
Stylistically, we often annotate module-level functions this way, instead:
#lang typed/racket
(: path-is-dot-git? (-> (U 'same 'up Path-For-Some-System) Boolean))
(define (path-is-dot-git? p)
(or (equal? p (string->path ".git"))
(and (not (symbol? p))
(path-has-extension? p ".git")
#t)))
It can be useful to explore the internal structure a type:
> (:type Path-For-Some-System)
(U OtherSystemPath Path)
> (:type Path-String)
(U Path String)
(Where OtherSystemPath is not public.)
This shows that Path is a subtype of Path-For-Some-System.
In general, you should be able to ignore Path-For-Some-System unless you specifically want to work with Windows paths on Unix (including Mac OS) or vica versa.
I'll start with Path and Path-For-Some-System; you say that I should be able to ignore the latter, and indeed this code will never have to deal with different systems; it'll always be working with Unix paths. So I want to just use Path everywhere, which looks cleaner and arguably reflects my intent better.
So in path-is-dot-git?, I now just accept a Path for its argument. Using my original code and that typing, the type is now (-> Path (U Boolean Bytes)) which works for me, I think, because when used with not, I get the expected (-> Path Boolean) type for the lambda function.
For the polymorphic first: I see in the documentation that I need to use inst. I'm not sure how to interpret the error message and turn that into the inst that I need, though:
in-git-repo.rkt:49:41: Type Checker: Polymorphic function `first' could not be applied to arguments:
Domains: (Listof a)
(Pairof a (Listof b))
Arguments: (Pairof Any Any)
in: (first path-components)
I have a Listof a, originally from explode-path; what sort of inst expression do I use there?
I've tried type annotations on rest-if-starts-with-dot-git, but I haven't been able to get it to work; I know that the actual types being used are Path and (Listof Path), but explode-path and others are typed with (U 'same 'up Path-For-Some-System) and lists of those.
It seems like I should let the typechecker do inference by somehow, early in the pipeline here, casting, or asserting, or whatever, something so that all the downstream code can be inferred to be working with Paths and lists of those.
What kind of type annotation or proposition could I use? How could I take an expression such as (explode-path (current-directory)) and tell the typechecker "I promise the output here has type (Listof Path)"?
Typed Racket doesn't do global inference for your whole file; in general you will need to write type annotations for each of your functions.
The basic problem with your code is that it doesn't handle the 'same and 'up results properly; this input causes it to crash: (get-git-repo-path-string "/one/two/../foo.git/../three") with an error about supplying 'up to path-extension=?. Typed Racket can help guide you to where you need to fix those problems but you will need to write down the types you want the functions to have.
Overall, I was expecting Typed Racket to work more like Typescript's inference and use similar code flow analysis, but it...doesn't. I don't have a good sense for how Typed Racket compares with Typescript, or how robust/sophisticated it really is.
I was never able to truly convince the typechecker that the code really does have Paths and lists thereof; above, @LiberalArtist said I should be able to ignore Path-For-Some-System, and I wanted to do that: it's awkward to type, and I'm not handling non-Unix paths. But I couldn't figure out how to do that: explode-path outputs a(Listof (U 'same 'up Path-For-Some-System)) and I don't see any way to coerce the elements of that list to true Paths.
But, using Path-For-Some-System throughout did work.
The other key thing, as I mentioned above, was that I needed to convince the type checker that we really will never have the symbols 'same or 'up here; doing that required filtering the is-path-for-some-system predicate over the list and including a proposition for that predicate so that it could infer that the filtered result was a list of Path-For-Some-Systems.
It looks like this is because Typed Racket doesn't give a sufficiently specific type to explode-path. Concretely:
> (:print-type explode-path)
(-> (U Path-For-Some-System Path-String)
(Listof (U 'same 'up Path-For-Some-System)))
> (:print-type split-path)
(case->
(-> Path-String (values (U 'relative False Path) (U 'same 'up Path) Boolean))
(-> (U Path-For-Some-System Path-String)
(values
(U 'relative False Path-For-Some-System)
(U 'same 'up Path-For-Some-System)
Boolean)))
Currently, split-path uses case-> to say that if its argument satisfies Path-String, it the relevant parts of its results will be Paths, whereas, if the argument is allowed to be the more general Path-For-Some-System, the results are also allowed to be Path-For-Some-System. In contrast, the type for explode-path isn't broken down by cases, so you have to handle the fully general result type.
In this case, we can open an issue for Typed Racket to give explode-path a more specific type, but I thought I'd show some approaches that can work around such problems in general.
Use require/typed
You can re-import explode-path and with the type you want:
(require/typed
racket/base
[explode-path (-> Path-String (Listof (U 'up 'same Path)))])
Typed Racket will use the contract system to ensure that untyped code satisfies the declared type, so, if you declare a type that misses some nuance of the actual behavior, you could get an error at runtime. Contract checking also introduces some performance overhead, though I wouldn't worry about it in this case.
Another catch is that you can't use require/typed to give more complete type we wish Typed Racket gave explode-path, because Typed Racket can't convert this kind of case-> type to a contract:
(case->
(-> Path-String (Listof (U 'up 'same Path)))
(-> (U Path-For-Some-System Path-String)
(Listof (U 'up 'same Path-For-Some-System))))
That's ok, though, because (-> Path-String (Listof (U 'up 'same Path))) is a subtype of the more complex type.
Re-implement explode-path
Occasionally, it can make sense to re-implement a simple helper function to make it visible to the type checker. You could shorten this by dropping the Path-For-Some-System cases, but I included them to show that this is fully general.
(define-type (Elements α) (Listof (U 'up 'same α)))
(: explode-path
(case->
(-> Path-String (Elements Path))
(-> (U Path-For-Some-System Path-String) (Elements Path-For-Some-System))))
(define (explode-path p)
(: loop (case->
(-> Path-String (Elements Path) (Elements Path))
(-> (U Path-For-Some-System Path-String)
(Elements Path-For-Some-System)
(Elements Path-For-Some-System))))
(define (loop p tail)
(define-values [base name _dir?]
(split-path p))
(if (path-for-some-system? base)
(loop base (cons name tail))
(cons name tail)))
(loop p '()))
Use occurrence typing
You already started down this road with your is-path-for-some-system and filter-symbols, but you did more work than necessary. Instead of is-path-for-some-system, you could just use the existing function path-for-some-system?. But you could also avoid Path-For-Some-System completely this way.
This is fundamentally different than the Path-For-Some-System issue, because there is no type-level distinction that can guarantee that you won't have . or .. components in a path.
You can use assert or extra filtering when you have some other way to know that certain cases will never happen, but I don't actually see anything in your program that does guarantee you won't have . or .. components. For example:
philip@bastet:/tmp/x/a/../b.git$ tree /tmp/x
/tmp/x
|-- a
`-- b.git
3 directories, 0 files
philip@bastet:/tmp/x/a/../b.git$ echo $PWD
/tmp/x/a/../b.git
philip@bastet:/tmp/x/a/../b.git$ racket
Welcome to Racket v8.17 [cs].
> (current-directory)
#<path:/tmp/x/a/../b.git/>
>
That example is weird and interesting. How did you do that? I can't get my shell to do the same thing. I tried symlinks for "a" and "b.git" inside "x" How did you do that? What shell are you using? I tried bash and zsh, and have never seen ".." in $PWD.
So, I was getting closer with the proposition on my filter predicate, but I was missing the path? function. I'll give that a try and see if I can simplify my code.
