Martin Baker wrote:
>
> I plan to have a new version of the computation framework soon
> (in time for this release).
> I am removing the VarTyp domain and using ILogic to represent
> types, that is: building Curry-Howard into the structure of
> the framework.
>
> I suspect that Curry-Howard has its limits, eventually it would
> be good to model anything in type theory including dependant
> types and I don't know if that would be possible using
> intuitionistic logic? In which case it might be be necessary to
> put VarTyp domain back in some stage in the (distant) future.
>
> If it would be a hassle for you to remove VarTyp, when there is
> a possibility it might be needed at some stage in the future, I
> could leave it in as a thin wrapper for ILogic. Perhaps you
> could let me know what you would prefer.
>
When removing things the main question is impact on other code.
Since VarTyp is closely tied to computation framework there
should be no impact on other code (=> no problem with removal).
I think it makes no sense to keep VarTyp "just in case it is
needed in the future" -- if you need to reintroduce something
like VarTyp is is likely that you will make changes compared
to current design and the result may be quite different.
--
Waldek Hebisch
[email protected]
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
