@lexi.lambda finally getting around to watching Inside Hackett!
I noticed the type checker structs are all prefab, I assume that is because of cross-phase uses?
I had a problem once where I wanted cross-phase structs but didn’t want them to be prefab so I could attach properties to them still (like custom write) and a method that ryan suggested was to declare a struct property in a cross phase persistent module and use that property in functions that I wanted to use in a cross-phase manner. Is that something you’d be interested in for those structs or is their prefab-ness not a problem?
@notjack I don’t think there’s any reason at the moment to make them non-prefab, but I could imagine a couple different ways to support that if it became necessary at some point.
gotcha
@lexi.lambda the transformation of a let to a lambda then back to a let - what problems come up if the lambda->racket-let step isn’t done and you just leave it as a lambda? is it for optimization reasons or something else?
you mean implementing let in terms of lambda? you could do that for let, specifically, but not for things like letrec or more complicated forms.
yeah I mean just for let specifically, no idea how to handle letrec
also is this the paper you were working off of? https://people.mpi-sws.org/~joshua/bitype.pdf
no, the paper is linked in the wiki page.
gotta make sure I add the right thing to the reading list :P
specifically, this paper: http://www.cs.cmu.edu/%7Ejoshuad/papers/bidir/
ah I missed the wiki page, thanks
@lexi.lambda Possible idea for the part of the hackett implementation that inserts @%dictionary-placeholder and then later performs a second expansion pass to insert the right dictionaries: what about using syntax-local-lift-expression and local-expand/capture-lifts? My thinking is that typeclass uses can use syntax-local-lift-expression to get an identifier for the dictionary they want and put their use-case-specific constraints in the lifted expression, then #%module-begin can call local expand, capture the lifted expressions, and manipulate the expressions to include the proper typeclass dictionary info based on the constraints in the lifted expressions. Do you think something like that could work?
and do you think it would be simpler than what hackett does currently
@notjack I don’t think that would work due to the way dictionary elaboration needs to consult local information introduced by @%with-dictionary.
@lexi.lambda what local information does dictionary elaboration need?
It needs (1) a fully solved type environment and (2) the set of constraints locally in scope.
The latter equivalently being the set of dictionaries in scope.
More generally, my long-term goal is to make the constraint solver extensible, so that things like type equalities, typeclasses, implicit parameters, checked exceptions, and units of measure can all be implemented separately from the core.
(And they can be mixed and matched.)
for things that are whole-program transformations, I’d expect the way to implement that would have to be as a #lang on top of hackett with the transformation implemented in #%module-begin somehow
did you have something different in mind?
bluntly, yes.
it’s not an unrestricted transformation, but I think the typechecker can provide hooks that allow the constraint domain to be extended in ways that add new source-to-source transformations, yet don’t sacrifice composition.
maybe something where hackett exposes lots of syntax parameters that influence how constraints are solved in a set of expressions?
I think it would be somewhat orthogonal to existing Racket metaprogramming constructs
interesting. in what ways? also, wild shot in the dark sort of question: do you think rosette or anything in its internals could be used in hackett’s implementation of constraint solving?
the idea behind much of hackett is using the typechecker as a way to propagate compile-time information that can then be used for metaprogramming. this is they key idea behind why I think hackett can, theoretically, do more than either racket or haskell.
(wrt metaprogramming, that is.)
right, no complaints with that here
I will touch upon that in some degree in my racketcon talk
as for rosette: I don’t know, but I doubt it.
they both use things called “constraint solvers”, but the sort of constraint solver used in haskell is a very different constraint solver from the one used in rosette. I am not sure the similarities extend beyond names.
if i wanted to write a liquid-hackett sort of thing that needed access to an SMT solver, rosette seems like something I’d poke at since it’s supposed to be for making langs that use SMT solvers to do stuff
but maybe for non-liquid-hackett it wouldn’t be useful at all
right, if you wanted to add the notion of refinements to hackett’s constraint domain, that might be useful. but the point is more that hackett ought to be agnostic to the constraint domain.
like HM(X) and OutsideIn(X) are parameterized over the constraint domain.
so it’d be more like hackett provides some sort of syntactic protocol for macros to declare, require, and influence constraints independent of what constraints actually are or how they’re checked
non-local constraints particularly
right. and one of the nice properties of the Haskell type system is that’s actually possible.
?
OutsideIn(X) provides an especially strong framework with an extensible constraint domain, but Hackett’s typechecker isn’t nearly as fancy as OutsideIn at the moment.
are HM(X) and OutsideIn(X) things in haskell’s internals that are exposed to language extensions?
but the fact that OusideIn works like that is encouraging, since it means Hackett can continue to be generalized even if it makes an extensible constraint domain a core, user-accessible feature.
I write very little haskell :p
I think GHC typechecker plugins can add new sorts of constraint solvers, but I don’t believe they can add new constraints.
OutsideIn(X) is the type system that GHC currently uses, though, for context.
ah so OutsideIn is this thing: https://wiki.haskell.org/Simonpj/Talk:OutsideIn
then is HM(X) a constraint domain agnostic type system that ghc used to use but doesn’t anymore?
for hindley milner I’m guessing :p
I don’t believe GHC ever used HM(X)
found this paper presenting HM(X): http://www.cs.tufts.edu/~nr/cs257/archive/martin-odersky/tapos-final.pdf
is there anything else worth reading about it for context?
I haven’t read that much about HM(X), since I’ve mostly focused on OutsideIn(X).
before OutsideIn, I believe GHC used a system known as “boxy type inference”
cute name
Hackett uses neither, since it uses a variant on Dunfield and Krishnaswami’s bidirectional system that’s similar to the PureScript typechecker
OutsideIn is very, very complex, but I think that’s largely because it’s designed to support type families, higher-rank polymorphism, and GADTs.
Hackett currently only supports one of those things.
lots to think about
thanks for entertaining my questions :P
really looking forward to the racketcon talk
a lot of this stuff is, of course, aspirational. I don’t yet know if all of it is even possible, and even if it is, I think it’d be new research.
the best kind of research
well, the only kind of research, I think.
if you know it’ll work, it isn’t really research, is it? :)
that would be the joke :p
in the past six months or so that I’ve been developing Hackett in earnest, I’ve developed some intuitions for certain things, so I think the ideas I have are possible, but I’m not 100% sure.
heh I still want to figure out how #lang hackett/script with submodules could work for writing main and test submodules, and also pull the infix op code out into a package so I can use it for other stuff
I thought about extracting the infix stuff, but it’s seriously like a couple dozen lines of code, and the interface isn’t stable enough for those couple dozen lines to be put in a package
plus, there are advantages to keeping Hackett monolithic right now.
not having to deal with racket’s package system and versioning is one that comes to mind
that’s part of it, but a larger part is that I can worry about implementing exactly what Hackett needs and nothing more.
true
helps keep focus
Hackett is, by LOC, extremely small.
hackett-lib is a mere 3047 LOC
heh, racket is amazing
hypothetically, if there was a package that implemented infix app syntax in such a way that hackett could use it, do you think using it would be a bad idea?
as of right now, probably. I think the time at which it might make sense to extract is once precedence is squared away, and that means we need to learn more about usage patterns for infix operators in real Hackett code.
seems reasonable enough to me
@jburgess84 has joined the channel