JacquesCarette / Drasil

Generate all the things (focusing on research software)
https://jacquescarette.github.io/Drasil
BSD 2-Clause "Simplified" License
142 stars 26 forks source link

Type checking error in pdControllers DifferentialModel: imPDRC #3104

Open balacij opened 1 year ago

balacij commented 1 year ago

Spawned from #3093

`imPDRC` exposes ill-typed expressions!
  - Inferred type `Boolean` does not match expected type `Rational`
  - Associative arithmetic operation expects all operands to be of the same type.
    Received:
      - ERROR: Associative arithmetic operation expects all operands to be of the same type.
      Received:
        - Real
        - Rational
        - ERROR: Associative arithmetic operation expects all operands to be of the same type.
        Received:
          - Real
          - Rational
          - Real

There are 2 equations exposed by imPDRC because it's a 'DifferentialModel'. We might need to re-evaluate what equations the differential models expose for type checking.

1st error: To my understanding, from the comments, DifferentialModels expose a series of equations, so they should all be boolean-typed Exprs:

https://github.com/JacquesCarette/Drasil/blob/3587dd15a468e3d9d7b90d344753d0fe3a0702c5/code/drasil-lang/lib/Language/Drasil/Chunk/DifferentialModel.hs#L129-L131

https://github.com/JacquesCarette/Drasil/blob/0a240c0231b6f737011bc090962ae1925fbc83e2/code/drasil-example/pdcontroller/lib/Drasil/PDController/IModel.hs#L23-L52

JacquesCarette commented 1 year ago

Current error is better:

`imPDRC` exposes ill-typed expressions!
  - ERROR: Inferred type `Boolean` does not match expected type `Real`
  - ERROR: Inferred type `Boolean` does not match expected type `Real`

So I'm not quite sure where the expected type is coming from. The Boolean is quite explicit in there (because it's an equation). Might this be a bug in the typechecker? @balacij

balacij commented 1 year ago

Hmm, I think you're right.

I think these are the relevant areas for understanding what needs type-checking.

https://github.com/JacquesCarette/Drasil/blob/77398324a45f8ea9ef6d8c5ec22cabaf6c931c77/code/drasil-lang/lib/Language/Drasil/Chunk/DifferentialModel.hs#L128-L130

Above, we say that we need to use the "formEquations" function to build a list of the equations, which is why I assumed they are all of type Boolean.

https://github.com/JacquesCarette/Drasil/blob/77398324a45f8ea9ef6d8c5ec22cabaf6c931c77/code/drasil-lang/lib/Language/Drasil/Chunk/DifferentialModel.hs#L275-L304

But, now, re-reading the comments of formEquations, it looks like I might have misunderstood what it does.

So, the Boolean in the RequiresChecking implementation might need to be the type of the dependent variable from the differential model (~ dmo ^. (depVar . typ)).

Re-running it, I get:

`imPDRC` exposes ill-typed expressions!
  - ERROR: Inferred type `Vect Rational` does not match expected type `Rational`
  - ERROR: Associative arithmetic operation expects all operands to be of the same expected type (Real).
    Received:
    - ERROR: Associative arithmetic operation expects all operands to be of the same expected type (Real).
      Received:
      - Real
      - Rational
    - ERROR: Associative arithmetic operation expects all operands to be of the same expected type (Real).
      Received:
      - Real
      - Rational
    - Real

Does this error make more sense in this context?

JacquesCarette commented 1 year ago

This does make more sense. And in current master, all those Rational are gone. I'm testing a fix now.

JacquesCarette commented 1 year ago

Now that the fix is in, now the error is

`imPDRC` exposes ill-typed expressions!
  - ERROR: Inferred type `Vect Real` does not match expected type `Real`
  - ERROR: Inferred type `Vect Real` does not match expected type `Real`

This is due to DifferentialModel's reconstruction of the system of equations being odd. Same bug as #3103.