Hacker News new | past | comments | ask | show | jobs | submit login

I heard F# supports this newish thing called dependent typing which allows the type checker to not only check for type correctness but logic correctness as well.

I've never worked with dependent typing but is it true? Does the F# really take away the need for all unit testing on a project?




F# does not support dependent typing. And in general, because it has to interop smoothly with .NET code written in C# and VB.NET, F# is not nearly as hardcore on functional purity as something like Haskell or Agda, and correspondingly cannot guarantee as much safety through its type system.

It is a wonderfully pragmatic language though and does guide the user towards more reliable software patterns than C# does. It sort of bridges the gap to be something you can actually use in production today, whereas the dependently typed languages are still in the realm of experimentation and toy projects for now.


Dependent typing generally doesn't play well with type inference (leading to things being all kinds of undecidable). I doubt it will ever make it's way into f#. GADT might, which provides a subset of the nice things of DT, but is much much easier to implement.

F* has dependent types though.


You are probably thinking of ‘F*’


You are thinking of OCaml and Coq.




Consider applying for YC's Spring batch! Applications are open till Feb 11.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: