MarcelineVQ 2017-02-09 09:45:31
what stack version?
tsahyt 2017-02-09 09:45:43
1.3.2
MarcelineVQ 2017-02-09 09:47:18
ah hmm, do you have cabal-install? stack needs that for it's solver afaik
Tuplanolla 2017-02-09 09:51:56
This cursed `hsc2hs` is nothing but trouble. Now it complains that a structure is undeclared even though it's right there.
sternmull 2017-02-09 09:51:57
i have a local stack "thingy" (don't know what it is called when you initialize it in a directory). In there i can not import System.Random. If i do it in a normal non-stack ghci i can import it. Do have have to declare System.Random as dependency in .cabal? I thought it is a standard package...
sternmull 2017-02-09 09:55:15
ah, ok. Had to add "random" to the build-depends. Shouldn't have asked so fast...
tsahyt 2017-02-09 09:57:29
MarcelineVQ: I should have it, but there might be a version problem
tsahyt 2017-02-09 09:58:55
sternmull: you need to declare all packages that you use in the cabal file, regardless of whether they are "standard" or not, even including base.
sternmull 2017-02-09 09:59:29
tsahyt: ok.
Tuplanolla 2017-02-09 10:01:02
Looks like I need to enable C11 for `hsc2hs` somehow.
Tuplanolla 2017-02-09 10:03:35
How do I tell `cabal` to tell `hsc2hs` to tell `gcc` to use `-std=c11`?
tsahyt 2017-02-09 10:04:50
Tuplanolla: gcc-options or so
tsahyt 2017-02-09 10:04:57
or cc-options
Tuplanolla 2017-02-09 10:06:58
Looks like `gcc` can find the definitions when called alone, but not through `hsc2hs`.
bollu 2017-02-09 10:13:05
what's the wildest type system that you guys know of? I've seen dependant typing and linear types, as well as structural typing. Are there others?
geekosaur 2017-02-09 10:13:15
hsc2hs-options: --cflag=-std=c++11
geekosaur 2017-02-09 10:13:16
or w/e
geekosaur 2017-02-09 10:13:33
Tuplanolla, ^
merijn 2017-02-09 10:13:49
Hah...that delightful moment where you dread writing some complicated code, only to realise it turns into a trivial handful of lines because Haskell is awesome :D
Tuplanolla 2017-02-09 10:14:57
That didn't help either, but removing `#{alignment ...}` did, geekosaur. It seems to be broken somehow.
geekosaur 2017-02-09 10:14:59
bollu, can't talk about wildest, but row types are another variety
bollu 2017-02-09 10:15:01
merijn: what were you coding?
bollu 2017-02-09 10:15:13
geekosaur: that is like Go, right?
kadoban 2017-02-09 10:15:21
bollu: Wildest? Does python count?
geekosaur 2017-02-09 10:15:23
and like sql
bollu 2017-02-09 10:15:39
kadoban: like, "sensible and interesting", not "fucked up"
merijn 2017-02-09 10:15:48
bollu: A mechanism that automatically determined the maximum request supported by the remote host by exponentially increasing until failure, then doing binary search
bollu 2017-02-09 10:16:06
merijn: and how did you code said thing? what's the code like? :)
bollu 2017-02-09 10:16:15
right now I'm reading about fractional and negaitve type
bollu 2017-02-09 10:16:17
types*
kadoban 2017-02-09 10:16:21
:)
merijn 2017-02-09 10:16:28
bollu: Well, I realised it basically devolves into two simple nested conduit loops :p
bollu 2017-02-09 10:16:31
I'm a man with a solution (SAT solvers) in search of a problem (type system)
merijn 2017-02-09 10:16:45
bollu: One to track maximum request size, the other to incrementally build request of that size
merijn 2017-02-09 10:16:54
and just use exception to deal with failure
bollu 2017-02-09 10:16:59
merijn: I see, interesting!
merijn 2017-02-09 10:17:10
bollu: You're not the first to apply SAT solvers to type systems
EvanR 2017-02-09 10:17:12
bollu: type systems are invented continually, each paper defines a new type system to present what its talking about
mniip 2017-02-09 10:17:19
bollu, system F-omega with explicit kind coercions?
merijn 2017-02-09 10:17:19
bollu: See the work on GHC's Nat kind
bollu 2017-02-09 10:17:28
merijn: I suppose I am not. Do you have references to older stuff?
bollu 2017-02-09 10:17:32
merijn: oh, interesting!
merijn 2017-02-09 10:17:38
bollu: LiquidHaskell too, afaik?
bollu 2017-02-09 10:17:40
mniip: go on. Isn't F-w undecidable?
bollu 2017-02-09 10:17:53
merijn: liquidHaskell is SMT, no? It uses it for more stuff
mniip 2017-02-09 10:17:56
oops
mniip 2017-02-09 10:17:58
not F-omega
mniip 2017-02-09 10:18:00
FC
merijn 2017-02-09 10:18:06
bollu: not sure
bollu 2017-02-09 10:18:18
mniip: what is that? I'm not "truly educated" in type systems :)
mniip 2017-02-09 10:18:36
have you seen 8.0's TypeInType yet?
bollu 2017-02-09 10:18:40
mniip: nope
mniip 2017-02-09 10:18:44
well
mniip 2017-02-09 10:19:03
type family KindOf a where KindOf (a :: k) = k
mniip 2017-02-09 10:19:12
promoted gadts
mniip 2017-02-09 10:19:20
and many other exciting things
bollu 2017-02-09 10:20:06
http://www.pm.ethz.ch/projects/student_docs/Matthias_Niklaus/Matthias_Niklaus_MA_paper.pdf: (Dec. 2005 - May 2006) well fuck, I'm a decade late
merijn 2017-02-09 10:20:24
I haven't decided whether I like TypeInType or am just confused as fuck by it
mniip 2017-02-09 10:20:40
merijn, there are good bits and there are bad bits
mniip 2017-02-09 10:20:54
like, it lets you do some cool stuff
mniip 2017-02-09 10:20:57
and you're like
bollu 2017-02-09 10:21:04
every time I think I have a new idea, I feel sad when I google it
mniip 2017-02-09 10:21:08
oh my, I have this idea, it's the coolest stuff ever
bollu 2017-02-09 10:21:16
idk how I will get a masters at this rate
mniip 2017-02-09 10:21:16
I wonder if the typesystem will allow me to---
mniip 2017-02-09 10:21:17
nope
mniip 2017-02-09 10:21:47
I'm not sure if it's incomplete or impossible
ralu 2017-02-09 10:21:48
arent type systems and computer algorithms isomorhic?
bollu 2017-02-09 10:22:04
ralu: how so?
skeuomorf 2017-02-09 10:22:05
ralu: programs and proofs
skeuomorf 2017-02-09 10:22:10
ralu: propositions and types
bollu 2017-02-09 10:22:12
ralu: type systems and logics are isomorphic
mniip 2017-02-09 10:22:22
at times it seems to defy the core haskell principle of composability
skeuomorf 2017-02-09 10:22:30
ralu: see: curry-howard isomorphism
skeuomorf 2017-02-09 10:22:36
ralu: propositions as types by philip wadler
bollu 2017-02-09 10:22:37
mniip: is * :: *?
mniip 2017-02-09 10:22:42
actually that seems to happen a lot with the new type system extensions
bollu 2017-02-09 10:22:43
mniip: like, do you get type universe tower?
mniip 2017-02-09 10:22:44
bollu, yes!
bollu 2017-02-09 10:23:01
mniip: so, I can encode Hott? :D
bollu 2017-02-09 10:23:06
or what little I know of it
mniip 2017-02-09 10:23:23
I know none of it so idk
mniip 2017-02-09 10:23:38
do note that the type universes are bounded from above
mniip 2017-02-09 10:23:51
by the amount of type variables you will bind or the amount of kinds you will specify
mniip 2017-02-09 10:24:11
you don't get "absolutely polymoprhic" variables
mniip 2017-02-09 10:24:27
only t1 :: t2 :: ... tn :: *
bollu 2017-02-09 10:24:41
mniip: what is the current haskell type system?
mniip 2017-02-09 10:24:54
haskell? or ghc
bollu 2017-02-09 10:25:08
mniip: ghc with everything on
bollu 2017-02-09 10:25:26
mniip: I remember asking a while back, and the best answer I got was "hindley milner, modified"
mniip 2017-02-09 10:25:30
I'm fairly sure this paper http://www.cis.upenn.edu/~justhsu/docs/nokinds.pdf
mniip 2017-02-09 10:25:38
maybe a few quirks appeared since
bollu 2017-02-09 10:26:21
is this based on outsidein?
bollu 2017-02-09 10:26:25
I found that a couple days back
geekosaur 2017-02-09 10:26:38
bollu, that would be true for standard Haskell (the modification is typeclasses). ghc is System Fc
geekosaur 2017-02-09 10:26:47
with modifications and constant tinkering >.>
merijn 2017-02-09 10:27:14
geekosaur: Not really anymore, though, is it?
merijn 2017-02-09 10:27:24
geekosaur: TypeInType is hardly System Fc?
geekosaur 2017-02-09 10:27:53
mm, true. but then I'm not sure we have a formal type system representing what ghc does any more
bollu 2017-02-09 10:28:22
geekosaur: is that not worrying?
geekosaur 2017-02-09 10:28:24
any grad students around that need a thesis? formalize current ghc >.>
geekosaur 2017-02-09 10:28:35
not really, no
geekosaur 2017-02-09 10:28:42
where do you think new type systems come from?
mniip 2017-02-09 10:28:53
the paper I linked above is goldfire's thesis iirc
mniip 2017-02-09 10:29:01
and it's the one implementing TypeInTyp4
bollu 2017-02-09 10:29:10
I see
bollu 2017-02-09 10:29:22
geekosaur: where do I need to go to learn type systems enough?
bollu 2017-02-09 10:29:27
I'm currently an undergrad, second year :3
geekosaur 2017-02-09 10:29:31
I have no idea
bollu 2017-02-09 10:29:33
enough of type systems*
bollu 2017-02-09 10:29:35
dang
merijn 2017-02-09 10:29:57
bollu: How much do you currently know?
bollu 2017-02-09 10:30:51
merijn: well, I understand the basic theory. I've played around with dependant types in idris, and with coq for theorem proving. I've implemented some bastardised version of algorithm w
merijn 2017-02-09 10:31:04
bollu: Have you looked at TaPL?
bollu 2017-02-09 10:31:07
merijn: and I've used dependant typing to encode matrices and all
bollu 2017-02-09 10:31:10
merijn: no, do tell
merijn 2017-02-09 10:31:15
@where tapl
lambdabot 2017-02-09 10:31:15
http://www.cis.upenn.edu/~bcpierce/tapl/
bollu 2017-02-09 10:31:40
why pierce :( I need to finish SF as well
mniip 2017-02-09 10:31:50
1486675264 [00:21:04] every time I think I have a new idea, I feel sad when I google it
merijn 2017-02-09 10:31:55
bollu: That should cover most of the basics and not-so-basics (i.e. from untyped lambda calculus) up to more than you need for Haskell2010
bollu 2017-02-09 10:32:03
I see
merijn 2017-02-09 10:32:11
bollu: From there on you've basically reached the point of "read papers"
bollu 2017-02-09 10:32:12
mniip: 'tis true
merijn 2017-02-09 10:32:26
Because there's no books that cover much more
bollu 2017-02-09 10:32:30
merijn: I see
mniip 2017-02-09 10:32:59
every time I do that, google finds nothing, but as I start putting some real effort into doing something with it,
bollu 2017-02-09 10:33:11
merijn: I will try and setup a reading group at college for this: we have a type systems prof who was at UPenn.
mniip 2017-02-09 10:33:11
someone links an obscure paper
merijn 2017-02-09 10:33:20
As for where to go to study this stuff: Oregan State University, Edinburgh, Strathclyde and a few other UK ones and Gothenburg in Sweden come to mind
monochrom 2017-02-09 10:33:44
It is OK if someone already wrote your idea in an obscure paper.
merijn 2017-02-09 10:33:45
bollu: Those are the first that come to mind w.r.t. having research groups on this stuff
merijn 2017-02-09 10:33:52
monochrom++
merijn 2017-02-09 10:34:08
You just steal the idea, minor repackage and write the well-known paper on it ;)
merijn 2017-02-09 10:34:26
mniip: Are you using Google Scholar?
mniip 2017-02-09 10:34:34
sometimes
merijn 2017-02-09 10:34:34
Regular google is useless for finding papers
monochrom 2017-02-09 10:34:36
For a historical example, everyone knows Hoare and his preconditions and postconditions. Did you know that he got it from an obscure paper of Floyd?
bollu 2017-02-09 10:34:37
merijn: I see, tankyou
bollu 2017-02-09 10:34:43
thank you*
mniip 2017-02-09 10:34:45
yeah sure
bollu 2017-02-09 10:35:01
merijn: right now, my life's trajectory is heading towards compilers and LLVM
merijn 2017-02-09 10:35:08
:)
bollu 2017-02-09 10:35:11
merijn: but I don't want to, like, "lose" type systems
qmm 2017-02-09 10:35:12
is it strange that cassava uses strict evaluation? https://github.com/hvr/cassava
bollu 2017-02-09 10:35:24
merijn: seriously :P I'll be working on compilers for the next couple months or so
monochrom 2017-02-09 10:35:34
Only difference being: Floyd did it on flow charts, Hoare brought it to program text.
vapid_ 2017-02-09 10:35:42
hey
vapid_ 2017-02-09 10:35:48
https://www.youtube.com/watch?v=cU8HrO7XuiE
merijn 2017-02-09 10:35:53
Unrelatedly, I wish I need less operators for haskell...hard to type with one hand when the cat is busy sabotaging my coding
vapid_ 2017-02-09 10:35:54
i really, really like this song
mniip 2017-02-09 10:36:55
I really want to find that paper now just to show what I'm talking about
bollu 2017-02-09 10:37:14
also, does anyone know of a way to compile a template instantiation machine output?
bollu 2017-02-09 10:37:22
I've been told that, like, G machine was created for this
bollu 2017-02-09 10:37:26
but are there any alternate strategies?
bollu 2017-02-09 10:37:43
also, question number 2: have there been efforts to mix lazy and strict evaluation?
bollu 2017-02-09 10:37:57
like, I wrote this: https://github.com/bollu/timi. I want to compile it using LLVM now
mniip 2017-02-09 10:41:02
http://ac.els-cdn.com/0167642389900361/1-s2.0-0167642389900361-main.pdf?_tid=69a95938-ef10-11e6-8942-00000aacb361&acdnat=1486676625_88ffb9e081b3ba923dfb360a9f023f5b
mniip 2017-02-09 10:41:11
look at the damn notation
mniip 2017-02-09 10:41:37
not even APL had that
dmwit 2017-02-09 10:42:35
Oh, well. Syntax used in papers is often ASCII-ized when doing an actual implementation.
bollu 2017-02-09 10:42:38
mniip: I remember seeing a book on "pattern calclus"
sternmull 2017-02-09 10:43:43
When i do "rs :: (RandomGen g, Random a) => g -> [a]; rs g = val:rs g' where (val, g') = random g" in ghci it says "Could not deduce (Random t0) ...". But it works when i compile it. Why is that?
sternmull 2017-02-09 10:44:16
(of course i imported System.Random)
mniip 2017-02-09 10:44:26
@hackage functional-kmp
lambdabot 2017-02-09 10:44:27
http://hackage.haskell.org/package/functional-kmp
mniip 2017-02-09 10:44:29
bollu, ^
qmm 2017-02-09 10:44:44
i have a list of strings and for each string, i want to insert it into the first column of a csv file
bollu 2017-02-09 10:44:50
has anyone seen this? fractional and rational types: https://www.cs.indiana.edu/~sabry/papers/rational.pdf
glguy 2017-02-09 10:44:53
sternmull: Because GHCi disables the monomorphism restriction
dmwit 2017-02-09 10:45:06
sternmull: Do you actually type it like that (with a semicolon), or do you type it on two lines?
