# Getting started with typed Racket and path-related types **URL:** \ **Category:** Questions & Answers\ **Tags:** question, typed-racket\ **Created:** [June 22, 2025, 8:49pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804 "2025-06-22T20:49:35Z")\ **Posts on this page:** 14\ **Page:** 1
**Author:** ![ddrake](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ddrake/32/2353_2.png) [@ddrake](https://racket.discourse.group/u/ddrake)\ **Post date:** [June 22, 2025, 8:49pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/1 "2025-06-22T20:49:35Z")
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. My code is here: [in-git-repo.rkt · GitHub](https://gist.github.com/dandrake/4b1d79ce9c75bf8ba57bb44e8c1ccd7f) 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: ```scheme 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? ---
**Author:** ![LiberalArtist](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/liberalartist/32/151_2.png) [@LiberalArtist](https://racket.discourse.group/u/LiberalArtist)\ **Post date:** [June 22, 2025, 9:40pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/2 "2025-06-22T21:40:55Z")
Here is an excerpt from your code that reproduces the first type error: ```scheme #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: ```scheme > (:print-type path-has-extension?) (-> (U Path-For-Some-System Path-String) (U Bytes String) (U Bytes False)) ``` The error: ```scheme 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: ```scheme #lang typed/racket (define (path-is-dot-git? [p : Path-String]) (path-has-extension? p ".git")) ``` Now, `path-is-dot-git?` has this type: ```scheme > (: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: ```scheme #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: ```scheme #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))) ``` * * * > [@ddrake](#): > > ```scheme > 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) > > ``` This error is explained by [§ 8.2 “Type inference for polymorphic functions”](https://docs.racket-lang.org/ts-guide/caveats.html#(part._.Type_inference_for_polymorphic_functions)) in _The Typed Racket Guide_. * * * > [@ddrake](#): > > Somehow, I think, I need to start with coercing between Path and Path-For-Some-System types. It can be useful to explore the internal structure a type: ```scheme > (: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. ---
**Author:** ![LiberalArtist](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/liberalartist/32/151_2.png) [@LiberalArtist](https://racket.discourse.group/u/LiberalArtist)\ **Post date:** [June 22, 2025, 9:51pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/3 "2025-06-22T21:51:09Z")
> [@LiberalArtist](#): > > But you pass `p` to `path-has-extension?`, which has this type: > > ```scheme > > (:print-type path-has-extension?) > (-> (U Path-For-Some-System Path-String) (U Bytes String) (U Bytes False)) > > ``` For posterity, this is a Typed Racket bug: the result type should actually be `Boolean`. > > > This program typechecks, but shouldn't, because \`x\` is \`#true\`: > \`\`\`racket > \#lang …typed/racket > (define x : (U Bytes False) > (path-has-extension? "a.git" ".git")) > \`\`\` > > The type of \`path-has-extension?\` is currently: > \`\`\`racket > (-\> (U Path-For-Some-System Path-String) (U Bytes String) (U Bytes False)) > \`\`\` > but the result type should actually be \`Boolean\`, the same as the documented contract. That bug doesn't affect these errors, though. ---
**Author:** ![ddrake](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ddrake/32/2353_2.png) [@ddrake](https://racket.discourse.group/u/ddrake)\ **Post date:** [June 23, 2025, 1:09pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/4 "2025-06-23T13:09:37Z")
Thanks for the reply! It's super helpful. I do have a lot of questions, though. 🙂 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: ```scheme 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? ---
**Author:** ![samth](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/samth/32/3_2.png) [@samth](https://racket.discourse.group/u/samth)\ **Post date:** [June 23, 2025, 1:35pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/5 "2025-06-23T13:35:20Z")
You most likely don't need an `inst` here, instead you need a type annotation on the `rest-if-starts-with-dot-git` function. ---
**Author:** ![ddrake](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ddrake/32/2353_2.png) [@ddrake](https://racket.discourse.group/u/ddrake)\ **Post date:** [June 23, 2025, 5:25pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/6 "2025-06-23T17:25:51Z")
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)`"? ---
**Author:** ![samth](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/samth/32/3_2.png) [@samth](https://racket.discourse.group/u/samth)\ **Post date:** [June 23, 2025, 5:53pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/7 "2025-06-23T17:53:35Z")
1. 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. 2. 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. ---
**Author:** ![ddrake](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ddrake/32/2353_2.png) [@ddrake](https://racket.discourse.group/u/ddrake)\ **Post date:** [June 24, 2025, 2:46pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/8 "2025-06-24T14:46:09Z")
I have it working! I updated [the gist with my working code](https://gist.github.com/dandrake/4b1d79ce9c75bf8ba57bb44e8c1ccd7f). Thank you, @LiberalArtist and @samth, for your help here. 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 `Path`s 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 `Path`s. 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](https://docs.racket-lang.org/ts-guide/occurrence-typing.html#(part._propositions-and-predicates)) for that predicate so that it could infer that the filtered result was a list of `Path-For-Some-System`s. ---
**Author:** ![LiberalArtist](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/liberalartist/32/151_2.png) [@LiberalArtist](https://racket.discourse.group/u/LiberalArtist)\ **Post date:** [June 24, 2025, 3:55pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/10 "2025-06-24T15:55:48Z")
> [@ddrake](#): > > 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 `Path`s. It looks like this is because Typed Racket doesn't give a sufficiently specific type to `explode-path`. Concretely: ```scheme > (: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 `Path`s, 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: ```scheme (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: ```scheme (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. ```scheme (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. ```scheme (: filter-explode-path (-> Path-String (Listof Path))) (define (filter-explode-path p) (filter path? (explode-path p))) ``` ---
**Author:** ![LiberalArtist](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/liberalartist/32/151_2.png) [@LiberalArtist](https://racket.discourse.group/u/LiberalArtist)\ **Post date:** [June 24, 2025, 4:08pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/11 "2025-06-24T16:08:07Z")
> [@ddrake](#): > > I needed to convince the type checker that we really will never have the symbols `'same` or `'up` here 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: ```scheme 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) # > ``` ---
**Author:** ![ddrake](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ddrake/32/2353_2.png) [@ddrake](https://racket.discourse.group/u/ddrake)\ **Post date:** [June 24, 2025, 9:28pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/12 "2025-06-24T21:28:36Z")
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. ---
**Author:** ![ddrake](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ddrake/32/2353_2.png) [@ddrake](https://racket.discourse.group/u/ddrake)\ **Post date:** [June 24, 2025, 9:33pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/13 "2025-06-24T21:33:59Z")
> [@LiberalArtist](#): > > # 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. > > ```scheme > (: filter-explode-path (-> Path-String (Listof Path))) > (define (filter-explode-path p) > (filter path? (explode-path p))) > > ``` Aha! That is almost certainly what I _really_ want here. And it does exactly what I had been trying to do with my flailing around: ```scheme > (filter-explode-path (current-directory)) - : (Listof Path) '(# # #) ``` 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. ---
**Author:** ![system](https://global.discourse-cdn.com/free1/uploads/racket/original/1X/4e853055ae989ed00f69341cd98bee95980776c4.png) [@system](https://racket.discourse.group/u/system)\ **Post date:** [June 27, 2025, 8:04pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/14 "2025-06-27T20:04:24Z")
---
**Author:** ![system](https://global.discourse-cdn.com/free1/uploads/racket/original/1X/4e853055ae989ed00f69341cd98bee95980776c4.png) [@system](https://racket.discourse.group/u/system)\ **Post date:** [June 27, 2025, 8:36pm UTC](https://racket.discourse.group/t/getting-started-with-typed-racket-and-path-related-types/3804/15 "2025-06-27T20:36:40Z")