10 ms·
An Introduction to Type Level Programming in Haskell
- turminal 5y agoThe best non-conventional introduction: https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview
- Zababa 5y ago> “Can I use any language?” > “Sure.” > Move quickly, before he realizes his mistake. This part always gets me.
- morty_s 5y ago> Criss is still here, at least physically. Got me.
- lelanthran 5y agoSeems to me that Lisp weenies have been outsmugged by Haskell weenies.
- Zababa 5y agoRead the next few ones, Lisp comes back strong.
- TeMPOraL 5y agoThanks for mentioning this. Both stories are lovely, some of the most enjoyable and intellectually satisfying writing I've read this month. On that note, I keep dreaming that one day, someone will make a Lisp with all the code generation goodies and Haskell-grade type system. That would be my dream language to code in. (As it is right now, I mostly do C++17 in overtly-type-safe style at work, and typed Common Lisp on the side...)
- thinkharderdev 5y agoThat may be the greatest thing I've ever read.
- hugsisbetter 5y agoPossibly inspired by https://codegolf.stackexchange.com/a/3790 https://codegolf.stackexchange.com/a/3790
- platz 5y agoThis uses the older/classic haskell 98 features to encode the types. It works, but with modern haskell, one can use techniques that are less verbose.
- deleted 5y ago[deleted]
- dfee 5y ago> Posted on August 25, 2021 by Rebecca Skinner > This blog post is a long-form article based on a talk I delivered at the haskell.love conference on 10 Sept 2021 Today, as far as I can tell, is Sept 9, 2021. Hello traveller from the future. Is time travel possible with Haskell?
- djur 5y agoI'd guess that the article was written after the talk was prepared but before it was delivered, and then it was updated after the talk was delivered.
- rebeccaskinner 5y agoThis is pretty much true- except the talk is actually in about 13 hours for now. I wanted to have the article ready as a companion piece as soon as the talk was done and opted to post it a couple of days early so that I wouldn’t need to worry about it and could enjoy the rest of the conference.
- dfee 5y agoRebecca, I enjoyed the article. Probably should’ve provided a less trite comment - but I figured this was the obvious. Sorry for forcing you to chime in on this, of all things. Good luck on the talk and enjoy the conf.
- lalaithion 5y agoYes: https://blog.csongor.co.uk/time-travel-in-haskell-for-dummies/ https://blog.csongor.co.uk/time-travel-in-haskell-for-dummie...
- Scarbutt 5y agoToday, as far as I can tell, is Sept 9, 2021. Depends on the country.
- bobdylan222 5y agoOther countries exist?!
- 12thwonder 5y agoback in the days, I had this infatuations with the idea of having everything checked at compile time by using type system. and I see many people following this kind of path with type system of Haskell, rust, and maybe typescript. granted, it feels good, at first. I don't do that any more. simply because I'm very lazy and also in a lot of cases, those types that I wrote will be replaced by more dynamic representation (e.g. strings) at some point.
- ebingdom 5y ago> I don't do that any more. simply because I'm very lazy I'm lazy too, but that's exactly why I use static types. So that when I refactor code, I can let the type checker tell me all the places that need to be updated instead of trying to piece that together from test failures (and praying that the tests didn't miss anything).
- 12thwonder 5y agoyeah, but my point is that checking system that you had created will be thrown away at some point in my experience. so why bother writing types? that is my attitude at least at very early stage of a project. later in a project where you know for sure something can be known at compile time, of course I love to check them at compile time.
- tikhonj 5y agoMy experience is that all my code gets thrown away or rewritten at some point. I've seen what code that doesn't get rewritten looks like; I'm intent on never inflicting anything like that on the world. As far as types go, I've found that types actually help more during prototyping than later on. (At least for code I've written myself; types are great for helping me navigate other people's long-term codebases!) Types give me a way to sketch out and iterate on an overall design without needing to implement anywhere near all the logic I'd need; then, when I start in on the logic, it naturally lays down on the skeleton the types provide. Compared to my experience with Python—where I still use some types!—I've found it easier to start and quickly try different designs in Haskell.
- ourcat 5y agoDespite the current https certificate issue, this is also a great introduction to Haskell. http://learnyouahaskell.com/chapters http://learnyouahaskell.com/chapters
- exdsq 5y ago+1 for the link, but I don't think type level programming should be an introduction to Haskell at all!
- dmitriid 5y agoSo, your programming with types. Do you also write tests with types? ;) In before "types check stuff". If you code some convoluted logic with types (and even non-convoluted logic, too), you still need to test that you've coded that logic correctly.
- danidiaz 5y agoI once coded red-black-trees in Haskell at the type level and yes, I had to write some type-level tests. In a real dependently-typed language the friction would be lower, because it's easier to put "normal code" at the type level. Perhaps I could have skipped some type-level tests by introducing more kind-safety...
- whateveracct 5y agoPeople do this actually. There's even best-in-class-level support for this in Haskell and Scala already: https://hackage.haskell.org/package/should-not-typecheck https://hackage.haskell.org/package/should-not-typecheck https://www.scalatest.org/scaladoc/3.2.0/org/scalatest/matchers/should/Matchers.html#checkingThatCodeDoesNotCompile https://www.scalatest.org/scaladoc/3.2.0/org/scalatest/match...
- dmitriid 5y agoThese two check that something doesn't type check. They don't really check the logic you've coded in your types (and which will type check). For example, a real-world situation from Turkey (looking at my check from Marks and Specner): goods from category 1 (clothes) have VAT of 8%, from category 2 have VAT of 18 % (plastic bag), and that if a person buys 2 items they get a 15% discount, and if they buy 3 items they get a 25% discount, and there are additional discounts on various goods. This will type check even if you code it as "if there is 1 item, do a 40% discount, and assign VAT of 2%".
- whateveracct 5y agoYou can test for things type checking just fine without special stuff. In Haskell type Test1 = TypeExpressionImTesting ~ ExpectedType Thus, you can also easily check type-level computation as well. A concrete example type AddTest = 2 + 2 ~ 4 ^ This is valid Haskell and will confirm the addition function does what you expect
- skybrian 5y agoThis is extraordinarily complex and admittedly contrived. In the end, it doesn’t do anything to help you pick good colors for your theme. It seems like support for live edits, so you can edit the theme with immediate feedback, is far more important than this sort of compile-time checking?
- eru 5y ago> It seems like support for live edits, so you can edit the theme with immediate feedback, is far more important than this sort of compile-time checking? Maybe. But this talk wasn't about the best way to pool a colour picker, I assume, but just used that one as an example for showing some programming techniques.
- skybrian 5y agoYes, I get that, but it would be nice to have a practical, non-contrived example, if one can be found.
- smegma2 5y agoThe article gives the following motivating example data AliceBlue = AliceBlue instance IsColor AliceBlue where toRGB = const $ RGB 0xF0 0xF8 0xFF My question is: can't we do away with the IsColor class and write: aliceBlue = RGB 0xF0 0xF8 0xFF I suppose we could imagine writing things that aren't RGB values, like CMY? Then my question is: how can we decide between writing a conversion layer (e.g. no type class, and past some boundary we deal with RGB values only, and the caller is expected to convert it) vs using the typeclass everywhere. I would tend to opt for the former but I'm curious to hear about the tradeoffs.
- eru 5y agoI suspect the answer is related to the Expression Problem. https://en.wikipedia.org/wiki/Expression_problem https://en.wikipedia.org/wiki/Expression_problem
- chrischen 5y agoWell that section she explicitly states this class allows for the abstraction over the color encoding (RGB vs CMYK, etc).
- smegma2 5y agoI understand that, but at some point someone will call toRGB. It seems like for any function that calls toRGB, we have a choice of using the existential type for this e.g. someFunc :: SomeColor -> ... someFunc (SomeColor color) = ... (toRGB color) ... vs having these functions accept an RGB instead of a SomeColor e.g. someFunc :: RGB -> ... someFunc color = ... color ... Then of course the caller would have to do the conversion someFunc (CMYToRGB color)
- chrischen 5y agoIt's likely that in this simple example the practical differences may be nonexistent. But if you think about the types represented and what they mean, RGB is not a color, but an encoding of a color. So if some function is supposed to take a color and RGB is used as a proxy for a color, you may very well be able to skip the abstraction but it would need to be refactored if you ever evolve into using the concept of a color and its presentation form in different ways. The class method seems to also allow CMYK and RGB to be defined completely independently of one another for any given color type. Whether that's necessary for the use case is beyond my understanding, but it allows that. I'd also imagine that giving colors their own types means that in the domain there's a small set of colors that are important, so a type class around this emphasizes the behaviors of these important colors rather than modeling a color system in general. Let's say one day RGB is superseded... while you can convert RGB values to any new value, you end up with all these functions that want to take a color, but are taking an RGB value instead. I do think that depending on the problem domain your method of treating colors as directly encoded values is valid, but maybe for a more robust color specific model than a color scheme application. I think a good analogy would be how to model a generic currency system, rather than the pricing plans of a SaaS app. The SaaS app will have some data StartupTier = StartupTier data ProTier = ProTier data EnterpriseTier = EnterpriseTier class IsPrice price where... instance IsPriceTier StartupTier where toUSD = const $ USD 5 Here it's not so much the currency system that we focus on than some discrete prices that we care about, that just so happen to convert to currencies. It also gives us the benefit of having tighter control on the different prices in different currencies rather than using a conversion function. Also that toRGB function has signature a -> RGB so it allows for a variable to perhaps dynamically calculate what RGB value it becomes... such as creating an instance of IsColor for something like "FavoriteColor" which could be pulled from the database.
- cjfd 5y agoI am not a haskell pogrammer but reading about monads it seems much ado about nothing. It seems that one does not need to understand category theory to understands monads. Basically, I would say, in very basic language, that a monad is a thing that swallows values so you cannot get them back. You can have one function that produces a value that is swallowed by the monad. Then you can compose these kinds of functions one after another and have all values swallowed by the monad. The use is e.g., to do output (IO monad) or do error handling (maybe monad). If you could get back your values from the output the output could be used to store state and functional programmers hate that so the output is a monad and cannot be used to get the state back.
- Twisol 5y agoIt depends on what you mean by "swallows values". If I have an IO<T>, I can very easily get at the T that's inside by flatMapping over it. It's true that there's no way to turn an IO<T> straight into a T -- whatever you do with the T must always get wrapped back in IO<-> at the end of the day -- but it's not gone, and indeed we do use monads to store state. (There's literally a monad called `State`, actually.) What monads don't let you get at -- at least, not without more knowledge about which monad you're using -- is whatever other information given alongside the Ts it contains. If I've got a random M<T>, and I don't know that M is Option, I can only operate over all the Ts (the either zero or one of them) it contains, but I can't tell whether it has any Ts in the first place.
- deleted 5y ago[deleted]
- fbn79 5y agoMy few word explanation: Monad is a wrapper for effectful impure functions. It swallow the effect (not value) and assure a defined value type to be available for further computing.
- PaulAJ 5y agoMonads are a unification of a bunch of computer stuff, including sequencing, IO, non-determinism, state, concurrency and exceptions. When I say "unification", I mean it in the sense that Newton's theory of gravity unified the motion of the planets with a falling apple (previously they were considered separate phenomena), or how Maxwell's equations unified electricity and magnetism. Once you grok monads you realise that all those different things I listed are just special cases of one overarching theory.