4 ms·
You’re overthinking it. In Idris, types can be computed. The RunLength data type is built such as if you give it a list, it gives you a (unique) type. And the
by rq1 5y ago
You’re overthinking it. In Idris, types can be computed.
The RunLength data type is built such as if you give it a list, it gives you a (unique) type.
And the only two constructors available are such that they enforce the encoding.
Try to unroll an example or build one from the definition and you’ll get it eg.:
How would you build an element of this type?
RunLength [1 1 1 3 3 7 7 7]
- skybrian 5y agoThe definition of RunLength looks like two functions for uncompressing a list, given that you already have all the data from within the compressed list. The output of the function is a type containing the uncompressed data. The input parameters to the "functions" appear to be data elements from within the compressed list. Because that's what they are. But this wasn't obvious to me. I think the weird bit is when the tags and fields within a datatype are represented using the same syntax as a function's name and parameters. This punning threw me off. I suppose the same is true in Haskell, but you don't write type constructors using '->' between the fields, so this punning is less obvious. (And Haskell's syntax for product types is itself less familiar to me than a 'struct' definition in a C-like language.)
- 4ad 5y ago> I suppose the same is true in Haskell, but you don't write type constructors using '->' between the fields, so this punning is less obvious That's exactly how you write GADTs in Haskell: https://downloads.haskell.org/~ghc/6.6/docs/html/users_guide/gadt.html https://downloads.haskell.org/~ghc/6.6/docs/html/users_guide....