Dependent typing and SMT solvers

[Jesper Nordenberg]

I'm a newbie to both dependent typing and SMT solvers, but I find both very useful improvements over type systems similar to those found in Haskell, ML, Scala etc. If I understand correctly one disadvantage of Idris and other dependently typed languages is that you have to write the proofs for logical predicates yourself (using tactics I assume), while in a language like LiquidHaskell an SMT solver is used to check the predicates. What are the advantages/drawbacks of either solution? Is Idris more powerful than LiquidHaskell (i.e. can you express and prove more things in the types)? Can you combine a language like Idris with an SMT solver to get the best of both worlds?

Interested in any points of view on the topic. Thanks!

/Jesper Nordenberg

[David Christiansen]

Hello Jesper

I really don't know enough about refinement types to say whether
something like Idris or something like Liquid Haskell can express more
properties.

I would like to combine Idris with an SMT solver that can check
postulated properties, as a kind of an extension of the type
providers, but I haven't gotten there yet.

In any case, it seems that both approaches are interesting areas of
research that may lead to very practical applications in the future.

/David

> --
> You received this message because you are subscribed to the Google Groups
> "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to idris-lang+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Jonathan Sterling]

Hello all,

Whilst refinement types hooked up to a solver can be a very cool thing,
it's important to remember that it greatly limits the sorts of
"refinements" one can make to precisely those which can be figured out
using the particular solver. Though perhaps in a language which already
has proper dependent types, such failures would simply result in the
creation of a new metavariable.

In addition, it's important to distinguish between refinement types
which are essentially a kind of subtyping extended with union and
intersection, from the resolution of proofs (which might be manual or
automated)...

My best,
Jon