7 ms·

Sounds good! I played with Idris quite a bit in the early days. I started spending more time in Coq around the time Idris gained its proof search mechanisms (I

Sounds good! I played with Idris quite a bit in the early days. I started spending more time in Coq around the time Idris gained its proof search mechanisms (I'm still not sure how they work!), but Idris has always been a more 'realistic' language for development (as opposed to proof engineering). I think I spoiled myself with dependent types, as all of my Haskell projects seem to hit a wall which dependent types can trivially solve (e.g. calculating a type or a TypeRep based on incoming JSON data)

hood_syntax 10y ago
Dependent types are the big win for me as well, even though I'm pretty inexperienced with both Haskell and Idris. I've heard LiquidHaskell thrown around when people talk about dependent types, have you looked into that before?
- chriswarbo 10y ago
  As far as I'm aware, LiquidTypes focus on very simple use cases, like length-indexed Vector types and such. I don't think it can manage "full" dependent types, for example situations I often find myself in where I want to calculate a type from incoming data, e.g. something like: parseJSON : String -> Maybe JSON parseJSON = ... parseMyData : JSON -> Maybe MyData parseMyData = ... HasSomeProperty : MyData -> Type HasSomeProperty x = case x of MyCase1 -> ... ... someProcessing : (x : MyData) -> HasSomeProperty x -> ResultOfProcessing x someProcessing x p = ... Often, we write "HasSomeProperty" such that it performs some arbitrary calculation to decide between returning the unit type ("does have this property") or returning the empty type ("doesn't have the property, or can't tell"). Whenever we need to provide a value of type "HasSomeProperty x", we just put a unit value and the type-checker will enforce that our arbitrary calculation resulted in a unit type. We can then use that property to access a bunch of functionality which the compiler would otherwise forbid us from using. This sort of code is trivial in a dynamically typed language: there's no requirement to prove anything, so we don't need any "HasSomeProperty x" values at all: we just go ahead and use whatever code we like, and hope that we didn't mess something up. We hit problems when we want to write our program in a language like Haskell with a (relatively) weak type system: the type system quite rightly forbids us from writing the unsafe version that dynamic languages would accept, but the language isn't expressive enough for us to (easily) encode the proofs required to convince the type checker that what we're doing is safe.
  - hood_syntax 10y ago
    Thanks for the writeup, broke it down nicely
  - lomnakkus 10y ago
    EDIT: ... or maybe I just misunderstood your example. If MyData is a statically known/defined type, then you can obviously accesss it however you want... but then I fail to see the value of HasSomeProperty returning a Type (given the reasoning below, you'd still have to have some proof object giving you the things you're interested in --- so that you wouldn't have to 'prove' the structure of the data obeys the property again.). I don't understand how you could possibly write any non-trivial (e.g. just unit-returning) code in the body of "someProcessing" with having some sort of proof object (generated by HasSomeProperty) with which to extract whatever you'd be interested in. As the example is written you'd only have a Type, but I don't see how that's enough. Can you explain or perhaps give an example of what a "someProcessing" function body might look like?
  - clusmore 10y ago
    >This sort of code is trivial in a dynamically typed language: there's no requirement to prove anything ... we just go ahead and use whatever code we like, and hope that we didn't mess something up. >the [Haskell] type system quite rightly forbids us from writing the unsafe version that dynamic languages would accept As somebody with familiarity with Haskell in the small but not in large applications, is it not similarly trivial to write in Haskell with the same level of safety that dynamic languages give you (i.e. explosion at runtime)? Consider as an example the following safe lookup function (standard Haskell) lookup :: Eq a => a -> [(a, b)] -> Maybe b lookup _ [] = Nothing lookup x ((a, b):abs) | a == x = Just b | otherwise = lookup x abs and the following unsafe lookup function lookup :: Eq a => a -> [(a, b)] -> b lookup x ((a, b):abs) | a == x = b | otherwise = lookup x abs How is the latter any worse than lookup in a dynamically-typed language where you are assuming the lookup will succeed (and hence don't write any error handling logic)? I know this sort of code is frowned upon in Haskell, but it can be done.
    - tome 10y ago
- trizinix 10y ago
  Richard A. Eisenberg has a nice comparison of Dependent Haskell with Idris and Liquid Haskell in his PhD. thesis[1]. There is a difference between refinement types and dependent types. In Liquid Haskell you basically state some predicates and then let the SMT solver figure out whether they are true. With Dependent Types you have to do all the legwork, but they are also more powerful. [1] https://github.com/goldfirere/thesis https://github.com/goldfirere/thesis
  - hood_syntax 10y ago
    Thank you for the recommendation
  - johncolanduoni 10y ago
    It's also important to note that you can embed SMT-driven refinement types into a fully dependently typed language; that's what F* does. I wonder how feasible doing something similar in Idris via the elaborator reflection and type provider faculties is. I remember Brady did something following a similar principle in one of the elaborator reflection papers with automated proofs of termination, but without calling into an external SMT solver.
codygman 10y ago
Could you link any simple examples on calculating a type or TypeRep based on incoming JSON data? One of my bigger interests in Haskell right now is the Frames library but I've honestly been struggling with using and understanding Template Haskell to generate Types. I haven't had a ton of time so it isn't all TH's fault either. I've also read the Template Haskell paper and the entire system seems well thought out, I suppose there just aren't enough practical tutorials I can mess about with until I understand.
- icen 10y ago
  (Not the OP) I don't know of any examples of using JSON to create types, but here [0] is a practical example of creating types dynamically from input, via writing a type-safe printf: [0]: https://youtu.be/fVBck2Zngjo https://youtu.be/fVBck2Zngjo
- chriswarbo 10y ago
  My most recent hack in this area is in [1]. We read in a bunch of type signatures from JSON and parse them with haskell-src-exts, but Haskell doesn't give us a way to turn these representations-of-types into actual types. The values we're constructing are to be passed into an API which requires all of its arguments to be Typeable, which it hides inside several layers of existentials (heterogeneous lists of heterogeneous maps of ...). Thankfully for our purposes there's an escape hatch: the values we provide won't be evaluated, so they can be `undefined`, and the `TypeRep`s generated from these values are only used for determining whether two types are (intensionally) equal or different. My solution was to define two new types, `Z` and `S a`, which can be used as peano numerals. We convert all of the distinct types in our JSON into distinct peano numeral types (`replaceTypes`), we generate `TypeRep` values for these numeral types (`getRep`), fabricate values of these types as arguments to the underlying library (`getVal`), then switch back all of the types which occur in the result (`restoreTypes`). Very ugly, but it works, thanks to the wiggle room I had based on what these types and values would be used for. Other projects have been even more icky, e.g. sending strings of auto-generated Haskell code through `runhaskell` [2] and throwing auto-generated template haskell into GHCi to see what sticks [3]. I don't recommend any of this for production code :) [1] http://hackage.haskell.org/package/reduce-equations http://hackage.haskell.org/package/reduce-equations [2] http://hackage.haskell.org/package/nix-eval http://hackage.haskell.org/package/nix-eval [3] http://chriswarbo.net/git/annotatedb/branches/master/annotatedb/runTypes.raw.html http://chriswarbo.net/git/annotatedb/branches/master/annotat...

hood_syntax 10y ago

Dependent types are the big win for me as well, even though I'm pretty inexperienced with both Haskell and Idris. I've heard LiquidHaskell thrown around when people talk about dependent types, have you looked into that before?

chriswarbo 10y ago
As far as I'm aware, LiquidTypes focus on very simple use cases, like length-indexed Vector types and such. I don't think it can manage "full" dependent types, for example situations I often find myself in where I want to calculate a type from incoming data, e.g. something like: parseJSON : String -> Maybe JSON parseJSON = ... parseMyData : JSON -> Maybe MyData parseMyData = ... HasSomeProperty : MyData -> Type HasSomeProperty x = case x of MyCase1 -> ... ... someProcessing : (x : MyData) -> HasSomeProperty x -> ResultOfProcessing x someProcessing x p = ... Often, we write "HasSomeProperty" such that it performs some arbitrary calculation to decide between returning the unit type ("does have this property") or returning the empty type ("doesn't have the property, or can't tell"). Whenever we need to provide a value of type "HasSomeProperty x", we just put a unit value and the type-checker will enforce that our arbitrary calculation resulted in a unit type. We can then use that property to access a bunch of functionality which the compiler would otherwise forbid us from using. This sort of code is trivial in a dynamically typed language: there's no requirement to prove anything, so we don't need any "HasSomeProperty x" values at all: we just go ahead and use whatever code we like, and hope that we didn't mess something up. We hit problems when we want to write our program in a language like Haskell with a (relatively) weak type system: the type system quite rightly forbids us from writing the unsafe version that dynamic languages would accept, but the language isn't expressive enough for us to (easily) encode the proofs required to convince the type checker that what we're doing is safe.
- hood_syntax 10y ago
  Thanks for the writeup, broke it down nicely
- lomnakkus 10y ago
  EDIT: ... or maybe I just misunderstood your example. If MyData is a statically known/defined type, then you can obviously accesss it however you want... but then I fail to see the value of HasSomeProperty returning a Type (given the reasoning below, you'd still have to have some proof object giving you the things you're interested in --- so that you wouldn't have to 'prove' the structure of the data obeys the property again.). I don't understand how you could possibly write any non-trivial (e.g. just unit-returning) code in the body of "someProcessing" with having some sort of proof object (generated by HasSomeProperty) with which to extract whatever you'd be interested in. As the example is written you'd only have a Type, but I don't see how that's enough. Can you explain or perhaps give an example of what a "someProcessing" function body might look like?
- clusmore 10y ago
  >This sort of code is trivial in a dynamically typed language: there's no requirement to prove anything ... we just go ahead and use whatever code we like, and hope that we didn't mess something up. >the [Haskell] type system quite rightly forbids us from writing the unsafe version that dynamic languages would accept As somebody with familiarity with Haskell in the small but not in large applications, is it not similarly trivial to write in Haskell with the same level of safety that dynamic languages give you (i.e. explosion at runtime)? Consider as an example the following safe lookup function (standard Haskell) lookup :: Eq a => a -> [(a, b)] -> Maybe b lookup _ [] = Nothing lookup x ((a, b):abs) | a == x = Just b | otherwise = lookup x abs and the following unsafe lookup function lookup :: Eq a => a -> [(a, b)] -> b lookup x ((a, b):abs) | a == x = b | otherwise = lookup x abs How is the latter any worse than lookup in a dynamically-typed language where you are assuming the lookup will succeed (and hence don't write any error handling logic)? I know this sort of code is frowned upon in Haskell, but it can be done.
  - tome 10y ago
trizinix 10y ago
Richard A. Eisenberg has a nice comparison of Dependent Haskell with Idris and Liquid Haskell in his PhD. thesis[1]. There is a difference between refinement types and dependent types. In Liquid Haskell you basically state some predicates and then let the SMT solver figure out whether they are true. With Dependent Types you have to do all the legwork, but they are also more powerful. [1] https://github.com/goldfirere/thesis https://github.com/goldfirere/thesis
- hood_syntax 10y ago
  Thank you for the recommendation
- johncolanduoni 10y ago
  It's also important to note that you can embed SMT-driven refinement types into a fully dependently typed language; that's what F* does. I wonder how feasible doing something similar in Idris via the elaborator reflection and type provider faculties is. I remember Brady did something following a similar principle in one of the elaborator reflection papers with automated proofs of termination, but without calling into an external SMT solver.

codygman 10y ago

Could you link any simple examples on calculating a type or TypeRep based on incoming JSON data? One of my bigger interests in Haskell right now is the Frames library but I've honestly been struggling with using and understanding Template Haskell to generate Types. I haven't had a ton of time so it isn't all TH's fault either. I've also read the Template Haskell paper and the entire system seems well thought out, I suppose there just aren't enough practical tutorials I can mess about with until I understand.

icen 10y ago
(Not the OP) I don't know of any examples of using JSON to create types, but here [0] is a practical example of creating types dynamically from input, via writing a type-safe printf: [0]: https://youtu.be/fVBck2Zngjo https://youtu.be/fVBck2Zngjo
chriswarbo 10y ago
My most recent hack in this area is in [1]. We read in a bunch of type signatures from JSON and parse them with haskell-src-exts, but Haskell doesn't give us a way to turn these representations-of-types into actual types. The values we're constructing are to be passed into an API which requires all of its arguments to be Typeable, which it hides inside several layers of existentials (heterogeneous lists of heterogeneous maps of ...). Thankfully for our purposes there's an escape hatch: the values we provide won't be evaluated, so they can be `undefined`, and the `TypeRep`s generated from these values are only used for determining whether two types are (intensionally) equal or different. My solution was to define two new types, `Z` and `S a`, which can be used as peano numerals. We convert all of the distinct types in our JSON into distinct peano numeral types (`replaceTypes`), we generate `TypeRep` values for these numeral types (`getRep`), fabricate values of these types as arguments to the underlying library (`getVal`), then switch back all of the types which occur in the result (`restoreTypes`). Very ugly, but it works, thanks to the wiggle room I had based on what these types and values would be used for. Other projects have been even more icky, e.g. sending strings of auto-generated Haskell code through `runhaskell` [2] and throwing auto-generated template haskell into GHCi to see what sticks [3]. I don't recommend any of this for production code :) [1] http://hackage.haskell.org/package/reduce-equations http://hackage.haskell.org/package/reduce-equations [2] http://hackage.haskell.org/package/nix-eval http://hackage.haskell.org/package/nix-eval [3] http://chriswarbo.net/git/annotatedb/branches/master/annotatedb/runTypes.raw.html http://chriswarbo.net/git/annotatedb/branches/master/annotat...