Any ideas why the effect system may be deprecated in favour of the state machine/indexed monads system? To me, they seem to be fulfilling two different requirements: algebraic effects let us call 'operations' in an expression by writing placeholder values, track the usage of such operations in the type, and plug in the implementation afterwards. For example, we can write "print" as a placeholder, give it a "StdOut" effect type, and provide a production implementation which writes to the program's stdout, a test implementation which produces a normal String value for us to check, a remote implementation which writes to a WebSocket, etc.
The state machine stuff seems to mostly be concerned with using types to keep track of state, in terms of which actions are available or unavailable, e.g. you can't close a file unless it's open, you can't read from a file unless it's open, you can't run an expression unless it closes all of its files, etc.
There's certainly overlap, but I'm not sure whether one subsumes the other.
Extensible effects arise from combining a free monad with an open union of functors. Using an indexed free monad with indexed functors instead is a generalization that provides more expressive power.
Intuitively, I like to think of it as:
- Extensible effects describe what we permit (read from console, print to console)
- Indexed monads describe what we demand (you must auth before you can access db, you must open file before you can read it)
Any more papers/resources I can look at to get more context on the indexed monads vs effect systems comparison? Are they as composable as effects - ie. how do they solve the problems with monad transformers, etc?
I think the proposal people are making is better thought of as indexed monads and effects rather than indexed monads or effects.
Normal extensible effects looks like:
data Union :: [Type] -> Type -> Type where
...
data Free :: (Type -> Type) -> Type -> Type where
...
type Eff fs = Free (Union fs)
class Inject f fs where
inj :: f a -> Union fs a
data File :: Type -> Type where
Open :: FilePath -> File ()
Close :: FilePath -> File ()
send :: (Inject f fs) => f a -> Eff fs a
-- The inferred type would be more general
openClose :: Eff '[File] ()
openClose = do
send (Open "foo.txt")
send (Close "foo.txt")
You can then generalize this by also indexing everything:
data HList :: [Type] -> Type where
Nil :: HList '[]
(:>) :: a -> HList as -> HList (a ': as)
data Union :: HList fs -> HList is -> HList is -> Type -> Type where
...
data Free :: (is -> is -> Type -> Type) -> is -> is -> Type -> Type where
...
type Eff fs = Free (Union fs)
class Inject f i o fs is os where
inj :: f i o a -> Union fs is os a
data FileStatus = Open | Closed
data File :: FileStatus -> FileStatus -> Type -> Type where
Open :: FilePath -> File 'Closed 'Open ()
Close :: FilePath -> File 'Open 'Closed ()
send :: (Inject f i o fs is os) => f i o a -> Eff fs is os a
-- The inferred type would be more general
openClose :: Eff (File ':> 'Nil) ('Closed ':> 'Nil) ('Closed ':> Nil) ()
openClose = do
send (Open "foo.txt")
send (Close "foo.txt")
Yes, that helps a ton! So it's simply combining extensible effects with state transitions to help you be more specific about the legal ways to sequence effectful operations.
The proliferation of type params looks intimidating from a user perspective though - is there some way to make it easier on folks? Would it look nicer in a language with row polymorphism perhaps?
The new States library is really a new implementation of Effects. It works in pretty much the same way, but emphasising the thing that the Effects library is best at and fixing some of its shortcomings.
There are two main differences at the moment:
- Everything has to be labelled
- There's no 'implicit' lifting of smaller sets of states
The first is annoying for things like Console IO, so I might change that. The second means that we have a much better chance of providing decent error messages, one day.
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)
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?
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.
>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.
> How is the latter any worse than lookup in a dynamically-typed language
Presumably you mean "better", not "worse". Well, it's better because you will (or should) get a compiler warning (or ideally an error) about the latter version.
I agree it's better, you will get a compiler warning about a partial function. I did actually mean worse though. The GP at least to me implied that Haskell (for cases like this) sits in the lowlands between Idris (and other dependently-typed languages) and dynamically-typed languages. Idris deals with the problem "the right way" by helping you guarantee that you deal with dynamic objects in a compile-time-guaranteed safe way, at the cost of some hassle of proving it is. Dynamically-typed languages deal with the problem "the practical way" by letting you pretend its safe so you don't have to go through the hassle of proving it is, at the cost of runtime safety. I think Haskell can also let you do this, it just feels wrong to do it as a Haskell programmer.
You're absolutely right that various hacks can be employed in Haskell; as well as missing branches, we can also exploit laziness to provide "undefined" or "loop = loop" expressions which, if we're right, won't ever be evaluated.
I didn't mean to imply that dynamic languages are "better" because they allow unchecked combinations of everything with everything else. Although I also didn't mean to imply that they're strictly "worse", precisely because there are things we can express easily in dynamic languages which take effort to reproduce in something like Haskell.
My main reason to mention dynamic languages was as motivation for why you might want to write such code in the first place: using dependent types to, say, prove Euclid's theorem of the infinitude of primes, would probably not motivate many software developers to give Idris a try. Examples like the type-safe printf mentioned in a sibling comment would presumably be much better motivators: we compute a type based on the format string, so providing a string like "Hello world %f %s !" will produce a type `Float -> String -> String` which accepts the required Float and String parameters, then returns the resulting String.
Off-topic, but related to undefined in Haskell, I love holes in Idris as a way to represent incomplete programs. I'd love if it somebody could take them one step further and have it so that if a hole is evaluated at runtime, a prompt came up and said "Well this is the input, what do you think the output should be?". You type it in, the program keeps going and a unit test is generated and put away somewhere for you to make sure that later when you implement it, you can help verify that you're doing it right.
> I'd love if it somebody could take them one step further and have it so that if a hole is evaluated at runtime, a prompt came up and said "Well this is the input, what do you think the output should be?"
For some cases, this is pretty simple to implement with unsafePerformIO - I've done that once or twice. Not a sin at all in development.
Heh, nice idea. Seems a long way off though. GHC semi-recently took a baby step in this direction by adding PartialTypeSignatures, although it emits a warning if you actually use them!
This makes sense on its own, but seems a bit silly when we consider that completely removing the signature will fix the warning ;)
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?
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.
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.
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.
(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:
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 :)
I've been learning Haskell and Idris off and on now for a few years. I have a few friends who happen to be computer science majors and they tend to be very dismissive of Haskell, they mostly focus on the performance tweaking of a Haskell program, which seems to be a 'black art'.
Does anyone know if Idris improves on this aspect of Haskell?
Idris, unlike Haskell, is strict, which has the general effect of making Idris' performance a bit more predictable, and a bit more like programming in other languages.
However, GHC is a phenomenal compiler, and can outperform Idris for many things; this is natural, as it's seen a lot of interest in terms of producing performant code.
There are still some gotchas in Idris code. The biggest one that I can think of is indexing some type with data that doesn't manage to get erased (the usual type erasure algorithm is pretty aggressive, but it can't remove everything). Some of the most useful types for programming (as in, proving theorems about the code) are wonderfully inefficient (as an example, the inductive definition of natural number is an empty linked list - taking up plenty of space in pointers, and killing your cache whenever it's accessed - Idris knows about Nat, but not about other types). Operations on the data, which might look very efficient, can also end up operating on the indices, which might not be.
I don't think Idris is nearly as performant as Haskell. Haskell has been around for way longer and has had piles of work done on optimizing the performance of the generated code, garbage collection, etc. Haskell can be written to be very fast, although its high-level nature and laziness can make it harder to optimize than a strict/imperative language.
Idris on the other hand is still very much an experimental project more focused on practical applications of dependent type theory than things like performance. However, with enough work done on its compiler, its strictness and the abundance of type information might allow it to be eventually more performant. Though, the lack of type erasure might negatively impact performance as well depending on how types work at runtime...
Would be nice to see a dependently-typed strict functional programming language that didn't require a GC or a C runtime. Are there any plans for this with Idris?
Function programming with no garbage collector is tough. There is a formalisation for dealing with this, called linear logic, which allows you to statically determine object lifetimes; but it's, um, a bit awkward. Such as, every value must be produced once and consumed once, so if you want to look at a variable, you need to produce a new variable with the same value (which must be consumed later).
The seminal linearly typed language is Linear Lisp, which is almost incomprehensible, and also a proof-of-concept which doesn't do anything useful. Classic paper here:
The closest thing to a modern language that uses them exclusively (Rust doesn't, by the way) is LinearML, which was an experimental toy, now abandoned. Tutorial here, which may be interesting:
In what way is Rust's use of affine lifetimes insufficient to implement "function programming with no garbage collection"? Genuine question, given my previous interest :)
In Rust you're allowed to look at values without consuming them, which pure linear typing doesn't support (it requires exactly one producer and exactly one consumer).
Also, in my experience, most Rust programs tend to stash stuff in reference-counted boxes whenever calculating lifetime gets complex; which is reasonable enough (C++ does the same thing), but it is basically garbage collection, and I'd like to find an expressive, functional, non-GCd language which doesn't require this.
We have plans to implement a framework for writing high performance, GC free programs in Lean (http://leanprover.github.io/). We have spent the last year addressing shortcomings of the previous version and will be shipping a new version early next year. The new features include a high performance proof automation framework, a native compiler, a profiler, a debugger, an incremental build system, a documentation tool, an FFI, including a bunch of goodies I am probably forgetting. We will be demoing Lean this year at POPL (http://popl17.sigplan.org/track/POPL-2017-Tutorials#program), and hope to cut a release ASAP.
You could look at ATS. I don't know a huge amount about it but I know it's a very high-performance bare-metal language with dependent types, or at least, more expressive types than Haskell/ML.
(Caveat: I've never written ATS, and although I've written in Coq and Idris, every time I look at ATS code it looks like complete gibberish).
Most of the ATS examples begin with something which looks like ML, but as the types are made more and more strict they end up looking like incredibly verbose C.
To make things worse, I don't think ATS has any inference either, so all of this must be written explicitly. Idris, Agda, Coq, etc. can infer types and values, if they're unambiguous.
For example:
Definition Prime p := forall n m, n * m = p -> n = 1 \/ m = 1.
All of these variables have type nat, which Coq can infer from the use of "*" and "=".
I’ve been working sporadically on a strict stack-based functional language called Kitten, with the goals of avoiding GC and libc. No plans for dependent types, but you might like to keep an eye on it anyway: https://github.com/evincarofautumn/kitten
This is pretty exciting. I'm still only about halfway through the book, but I am really enjoying the language. Learning it has been a real brain melter (in a good way) so far. Am looking forward to finishing the book.
I do appreciate how you can use dependant types as much or as little as you like, so in some ways it can actually be considered a simpler and easier to learn Haskell due to having strict evaluation.
Great to see. Idris is pretty much the final frontier for what I see value in becoming comfortable with as far as functional programming goes. Hopefully it gets more momentum moving forward.
Quick question, does design by contract, ie. invariants and so on, warrant calling dependent typing? I'm currently learning OCL, and Haskell next, hence the question.
The state machine stuff seems to mostly be concerned with using types to keep track of state, in terms of which actions are available or unavailable, e.g. you can't close a file unless it's open, you can't read from a file unless it's open, you can't run an expression unless it closes all of its files, etc.
There's certainly overlap, but I'm not sure whether one subsumes the other.