typecheck not working

[Giuliano Lancioni]

Hello,

I have been trying the type checking examples in the tutorial, but the shell (both Haskell and C) seems to reject the -typecheck option with pt. I get the error:

option not interpreted: typecheck

Has the typecheck option been removed from put_tree?

Thank you,

Giuliano

[Giuliano Lancioni]

Ok, I think the issue was already discussed in this old post:

https://groups.google.com/forum/#!searchin/gf-dev/pt%7Csort:date/gf-dev/LoCoWx0EQqQ/kkBws9pWq6gJ

Yet I cannot understand if there exists a way to check dependent types in current build or if some other strategy should replace the one shown in the tutorial.

Thanks!

[Krasimir Angelov]

Types are always checked since type incorrect trees might lead to runtime errors. That is why there is no pt -typecheck option. Where was that written? 

Btw. Dependent types were never fully implemented so I wouldn't count on them.

--

---
You received this message because you are subscribed to the Google Groups "Grammatical Framework" group.
To unsubscribe from this group and stop receiving emails from it, send an email to gf-dev+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/gf-dev/64b0f49d-71d0-475f-9190-2c13a8246400%40googlegroups.com.

[Giuliano Lancioni]

Thank you, Krasimir.

Reference to pt -typecheck is in the Tutorial:

Solving metavariables

Use the command put_tree = pt with the option -typecheck:

    > parse "dim the light" | put_tree -typecheck
    CAction light dim (DKindOne light)

The typecheck process may fail, in which case an error message is shown and no tree is returned:

    > parse "dim the fan" | put_tree -typecheck
  
    Error in tree UCommand (CAction ? 0 dim (DKindOne fan)) :
      (? 0 <> fan) (? 0 <> light)

Il giorno martedì 10 dicembre 2019 08:34:54 UTC+1, kr.angelov ha scritto:

Types are always checked since type incorrect trees might lead to runtime errors. That is why there is no pt -typecheck option. Where was that written? 

Btw. Dependent types were never fully implemented so I wouldn't count on them.

На пн, 9.12.2019 г., 23:38 Giuliano Lancioni <glan...@gmail.com> написа:

Ok, I think the issue was already discussed in this old post:

https://groups.google.com/forum/#!searchin/gf-dev/pt%7Csort:date/gf-dev/LoCoWx0EQqQ/kkBws9pWq6gJ

Yet I cannot understand if there exists a way to check dependent types in current build or if some other strategy should replace the one shown in the tutorial.

Thanks!

Il giorno lunedì 9 dicembre 2019 22:44:51 UTC+1, Giuliano Lancioni ha scritto:

Hello,

I have been trying the type checking examples in the tutorial, but the shell (both Haskell and C) seems to reject the -typecheck option with pt. I get the error:

option not interpreted: typecheck

Has the typecheck option been removed from put_tree?

Thank you,

Giuliano

--

---
You received this message because you are subscribed to the Google Groups "Grammatical Framework" group.

To unsubscribe from this group and stop receiving emails from it, send an email to gf-...@googlegroups.com.

[Giuliano Lancioni]

What is happening now is that dependent types are checked when parsing in the Haskell shell, but not in the C shell (or C bindings).

[Krasimir Angelov]

There are dependent types in the Haskell runtime but to make everything reliable and easy to use more work in borh the compiler and the runtime is needed.

На вт, 10.12.2019 г., 11:06 Giuliano Lancioni <glan...@gmail.com> написа:

What is happening now is that dependent types are checked when parsing in the Haskell shell, but not in the C shell (or C bindings).

--

---
You received this message because you are subscribed to the Google Groups "Grammatical Framework" group.
To unsubscribe from this group and stop receiving emails from it, send an email to gf-dev+un...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/gf-dev/a770c2b4-3d33-4cf4-b53e-18b9754f5bec%40googlegroups.com.