I'm David Feuer. I maintain containers, co-maintain unordered-containers and pqueue, and contribute to various other projects. Data structures are fun. I'm a good person to talk to about laziness subtleties, and about whether particular applications of unsafe IO are safe in context.
I'll kick this off. My name is Jaro. I have been interested in Haskell for about 8 years now. I like it because of it's connections to theory; there is always more to learn!
I'm currently working on gigaparsec which is a parser combinator library like parsec and megaparsec, but gigaparsec allows you to write your parser in a natural left-recursive way and it returns all possible parses instead of just the first parse that succeeds. My goal is to make a parser combinator library that allows you to use annotations to inform the parsing process instead of forcing you to restructure your parser.
Recently, I'm getting more and more convinced that correctness is the cornerstone of computation. To write a useful program you should first specify the idea itself and only later provide an efficient implementation. I got this idea from Conal Elliot who has talked about it on the Type Theory Forall podcast and recently at ZuriHac.
So, now I've also started reading the HoTT book to see what it really takes to express myself formally.
I don't really like having my work end up in proprietary software, but if there are people that would be willing to contribute only if I license it more permissively then I would consider that. For now I think there is still a long way to go before such issues will arise.
I'm always surprised by how much controversy there is online about laziness and space leaks, but almost all these industry interviews from Serokell includes lines such as:
Mats: Most of the things that people warn online such as laziness, memory leaks, hiring haven’t been problems so far. The biggest problem we have faced relates to upgrading the dependencies.
This was a fun episode. I was introduced to breadth first labeling and attribute grammars by Doaitse Swierstra at the Applied Functional Programming summer school in Utrecht. He was an inspiring figure.
The biggest disadvantage of circular programs is that it is very easy to get into infinite loops when you make mistakes. I wish there was an easy way to guarantee statically that circular programs are terminating (perhaps using types).
I think Idris' bang notation for performing effects in a do-block is pretty, it could look like this:
main = do putStrLn ("You said: " ++ !getLine)
Today, you'd have to come up with a new variable name or figure out the right combinator names:
main = do line <- getLine; putStrLn ("You said: " ++ line)
main = putStrLn . ("You said: " ++) =<< getLine
But unfortunately there are more complicated cases:
main = do print (True || !getLine == "foo")
In a strict language with built-in short-circuiting logical operations the getLine would never be performed, but in Haskell || is just a normal function that happens to be lazy in its second argument. The only reasonable way to implement it seems to be to treat every function as if it was strict and always perform the getLine:
main = do line <- getLine; print (True || line == "foo")
Do you think this is confusing? Or is the bang notation useful enough that you can live with these odd cases? I'm not very happy with this naive desugaring.
@jaror@bss03 Maybe I was wrong, but I think you can do Scott encoding of the GADT underneath the standard codensity representation of existentials via CPS. Still need higher-rank types, not "just" parametricity.
I should write up some code to check myself against GHC.
You can swap out x for y to see the behavior is the same.
You can drop the GADT pragma, GADT definition, f, existential, g, and x (but keep all the Scott versions, includeing y) to reveal code that works “simply” with RankNTypes.
Higher-rank types and parametricity is quite powerful.
BTW, this isn’t new / doesn’t require the bleeding edge compiler. I’m on “The Glorious Glasgow Haskell Compilation System, version 9.0.2” from the Debian repositories.
The Lemmy->Kbin conversion has inserted a lot of <span> elements into your code making it unreadable. For people reading this from the Kbin side, here's the code:
{-# language GADTs #-}
{-# language RankNTypes #-}
import Data.Functor.Const
-- The GADT
data AGADT a where
I :: [Integer] -> AGADT Integer
S :: String -> AGADT String
type Scott_GADT a = forall fr. ([Integer] -> fr Integer) -> (String -> fr String) -> fr a
f :: AGADT a -> String
f (I x) = show x
f (S x) = x
f' :: Scott_GADT a -> String
f' x = getConst $ x (Const . show) Const
-- The Existential
data AnyGADT = forall a. MkAnyGADT (AGADT a)
type Scott_Any =
forall r.
(forall a. (forall fr. ([Integer] -> fr Integer) -> (String -> fr String) -> fr a) -> r) ->
r
g :: String -> AnyGADT
g "foo" = MkAnyGADT (I [42])
g "bar" = MkAnyGADT (I [69])
g x = MkAnyGADT (S x)
g' :: String -> Scott_Any
g' "foo" x = x (\i _s -> i [42])
g' "bar" x = x (\i _s -> i [69])
g' s x = x (\_i s' -> s' s)
main = interact (unlines . fmap x . lines)
where
x s = case g s of { MkAnyGADT x -> f x }
y s = g' s f'
I think the spans are all syntax highlighting/coloring. Your comment seems to have a dangling ```/span at the end to me, but that might just be the KBin->Lemmy translation.
EDIT: Also, Lemmy seems to be munging this post between the preview and the submit, due to me wanting to include some text that appears to be a dangling xml/html end tag (angle brackets removed in edit for “readability”) inside backticks.
Ah, that's interesting. Although I can imagine not many people would want to write code in that style. And I also wonder how many languages support higher rank polymorphism in the first place.
Yeah, I generally prefer pattern matching and constructor calls, but often languages don’t have GADTs or existentials. Even in GHC, existentials are still a bit “wonky”, though still generally nicer to use than CPS/Codensity.
@jaror yes very nasty, I reported an issue and three bugs were found investigating it. Romes and Ben did great work doing so. It were multiple issues with pointer tagging.
Haskell
Top