GADT type system #23
GADT type system #23
Conversation
wzwietering
added
wontmerge
There was a problem hiding this comment.
Hey @wzwietering this is really cool! 👀 Thanks a lot for the demo of how the explicit mode works, this is very big work you did! I am a little unsure if I follow the motivation for this change and which parts of the Type System, that are mentioned in the PR description, are affected? I really like the work and added explicitness of this approach, but if we could discuss the idea a bit better, that'd be super nice, I think I am missing a few pieces 🤔
| @@ -0,0 +1 @@ | |||
| Hello world. This file is written to test the expansions of kb_example.csv. We should see that hello is expanded to hello. This is a theorem, which we cannot proof. No lemma or axiom can be used, because this is not a scientific theorem. | |||
There was a problem hiding this comment.
This looks like a little overlap with #22 PR. So I am not sure if there is a technical dependency between them or is it a continuation of the other? Is it safe to merge both or are they alternatives?
| Nothing -> error "No input file was found" | ||
| Just f -> do | ||
| s <- readFile f | ||
| returnOutput (out c) (decode $ mapParseStructure getKnowledgeBase $ doParse s) |
There was a problem hiding this comment.
This is cool! Although I am not certain I follow fully why this change to the "Explicit" mode was necessary? 🤔 It's sure possible that I am missing something. Could you make elaborate a bit on the motivation?
If you check the comment on #22 (this one), this looks very similar to what I wrote there :))) I'm not sure if one or the other approach is easier/more reliable so please let's check this out? :))
| case xs of | ||
| Exp ex -> handleExpMode ex | ||
| Kbt kbt -> handleKbtMode kbt | ||
| Hlp -> print $ helpText [] HelpFormatAll arguments |
There was a problem hiding this comment.
Cool! This is really fun to see the explicit mode, I like it, but at the same time, it appears a bit more verbose, which is both a good thing (more explicit), but also I am not sure if this makes it more complicated to maintain in the future. I'm all pro going with this approach if there's a clear advantage!
There was a problem hiding this comment.
The only advantage is that we can define our custom handlers, but I dislike the verbosity and maintenance it will cause
| data Expand | ||
| = Expand | ||
| { expand_abbr :: String | ||
| , expand_kb :: Maybe FilePath |
There was a problem hiding this comment.
why do we add prefixes to the record attributes in these cases? I think they don't overlap with other records in any case, so this shouldn't be a problem IIRC? I might be missing something ofc.
There was a problem hiding this comment.
There was a name clash error. I don't recall the exact one
| ,flagReq ["abbr"] (updateMode "delete_abbr") "abbreviation" "Abbreviation" | ||
| ,flagHelpSimple helpMode | ||
| ] | ||
| where initial = Kbt $ Del $ Delete { delete_abbr = "", delete_kb = Just "" } |
There was a problem hiding this comment.
Wow man, this is a lot of work!!!! 👀 Dude, you're a machine, thanks for investing all the time here 🚀
| updateMode "update_ex" s (Kbt (Up r)) = Right $ Kbt $ Up $ r { update_expansion = s} | ||
| updateMode "update_abbr" s (Kbt (Up r)) = Right $ Kbt $ Up $ r { update_abbr = s} | ||
| updateMode "delete_kb" s (Kbt (Del r)) = Right $ Kbt $ Del $ r { delete_kb = Just s} | ||
| updateMode "delete_abbr" s (Kbt (Del r)) = Right $ Kbt $ Del $ r { delete_abbr = s} |
There was a problem hiding this comment.
I am not sure I can follow fully what this does? 👀 😓
There was a problem hiding this comment.
updateMode is a somewhat magical function that updates records. It uses a magic string and a pattern match to update values. Lenses would be better here, but getting that approach working here took me too much time.
| returnOutput :: Maybe FilePath -> String -> IO () | ||
| returnOutput f = case f of | ||
| Nothing -> error "No output file found" | ||
| Just s -> writeFile s |
wzwietering
added
the
wontmerge
Improved type system. CmdArgs had to be changed to explicit mode for the new type system to work.