jle` 2017-02-24 12:54:56
erisco: yeah you can definitely do this at the type level
jle` 2017-02-24 12:55:08
i think there might be some libraries that already have them
erisco 2017-02-24 12:55:10
what about proving the associativity of const, gr
jle` 2017-02-24 12:55:29
what are those
erisco 2017-02-24 12:55:40
by gr I mean grrrrr
jle` 2017-02-24 12:55:48
actually i've directly used these types
jle` 2017-02-24 12:55:52
sometimes i've defined them from scratch
erisco 2017-02-24 12:56:10
the two in question are both simple
erisco 2017-02-24 12:56:17
but all good inductive definitions are :)
jle` 2017-02-24 12:56:22
data All :: k -> [k] -> Type
jle` 2017-02-24 12:56:34
AZ :: All a '[]
jle` 2017-02-24 12:56:44
AS :: All a as -> All a (a ': as)
jle` 2017-02-24 12:56:52
data Any :: k -> [k] -> Type where
erisco 2017-02-24 12:57:36
I don't know why you do not instead have All :: '[k] -> Type
jle` 2017-02-24 12:57:50
All (== x), some type
jle` 2017-02-24 12:58:01
so your original one would be All 'True
jle` 2017-02-24 12:58:20
AnyZ :: Any a (a ': as)
jle` 2017-02-24 12:58:38
AnyS :: Any a as -> Any a (b ': as)
jle` 2017-02-24 12:58:42
any is often called 'Index
jle` 2017-02-24 12:58:44
'
jle` 2017-02-24 12:58:50
http://hackage.haskell.org/package/type-combinators-0.2.4.3/docs/Data-Type-Index.html
jle` 2017-02-24 12:59:35
and All i've called Uniform before
jle` 2017-02-24 13:00:00
you can even do some skolemization here which is kinda cute
jle` 2017-02-24 13:02:08
er i can't figure it out right now
erisco 2017-02-24 13:02:23
maybe All :: (p :: a -> *) -> [a] -> Type AZ :: All p '[] AS :: p x -> All p xs -> All p (x ': xs)
jle` 2017-02-24 13:02:58
SkolemAll :: (Any a as -> a :~: b) -> All b as
jle` 2017-02-24 13:03:00
there ya go
jle` 2017-02-24 13:03:19
er no that's wrong
jle` 2017-02-24 13:03:54
data All a as = All (forall b. Any b as -> a :~: b)
erisco 2017-02-24 13:03:59
that corresponds to all :: (a -> Bool) -> [a] -> Bool
erisco 2017-02-24 13:05:35
All ((:~:) 'True)
erisco 2017-02-24 13:07:41
then you can have lists of even naturals and all sorts of stuff :)
jle` 2017-02-24 13:08:40
is there any way i can change the type of 'a -> Maybe b -> (c, d)' to show that 'c' cannot depend on the 'Maybe b' ?
jle` 2017-02-24 13:08:55
originally i had `a -> (c, Maybe b -> d)`, but...there are issues.
jle` 2017-02-24 13:09:19
that might be complicated to explain and are very specific to my application heh
jle` 2017-02-24 13:09:40
but 'a -> Maybe b -> (c, d)' works, i'm just not happy that the type is less descriptive
erisco 2017-02-24 13:10:17
I have encountered this before and unfortunately I don't know
jle` 2017-02-24 13:10:21
(a -> c, a -> Maybe b -> d) would be as descriptive
jle` 2017-02-24 13:10:27
but is unideal because it requires recomputing things
erisco 2017-02-24 13:10:41
there is this notion of intermediate values
jle` 2017-02-24 13:10:46
hm this actually looks like a similar pattern to lens
jle` 2017-02-24 13:11:04
maybe i can van laarhoven this up
MarcelineVQ 2017-02-24 13:11:39
ordoesit :O can join points cut the recomputing
jle` 2017-02-24 13:11:43
laarhovenization
phz_ 2017-02-24 13:12:39
god I feel stupid
phz_ 2017-02-24 13:13:10
I have stack complaining about a dep:
phz_ 2017-02-24 13:13:21
vector: needed (>=0.12 && <0.13), 0.11.0.0 found (latest applicable is 0.12.0.0)
phz_ 2017-02-24 13:13:42
so I just tried a
phz_ 2017-02-24 13:14:22
stack install 'vector-0.12.0.0'
phz_ 2017-02-24 13:16:39
Error parsing targets: Specified target version 0.12.0.0 for package vector does not match snapshot version 0.11.0.0
phz_ 2017-02-24 13:16:39
wtf?
erisco 2017-02-24 13:16:39
newtype Intermediate a b c = Intermediate (a -> (b, c)) maybe you can make something happen with it
phz_ 2017-02-24 13:16:39
any idea?
MarcelineVQ 2017-02-24 13:16:39
phz_: I looks like the snapshot you're using has 0.11.0.0 but you need at least 0.12.0.0 so you either need to add the version you want to extra-deps so it pulls it from hackage or you need a newer lts
erisco 2017-02-24 13:16:39
Intermediate a c (Intermediate (Maybe b) d ())
phz_ 2017-02-24 13:16:39
MarcelineVQ: lts-8.2
erisco 2017-02-24 13:17:57
but guided
jle` 2017-02-24 13:25:38
the problem is that the intermediate state is the state of an ST computation
jle` 2017-02-24 13:25:38
and all of its STRefs
jle` 2017-02-24 13:25:38
if I could somehow freeze the state...
recursion-ninja 2017-02-24 13:34:52
I'm trying to `stack build` with the `-debug` flag passed to GHC but it fails with a linking error: "/usr/bin/ld: cannot find -lHSrts_debug_p"
recursion-ninja 2017-02-24 13:35:13
Any ideas on how to pass the library to ld?
wedify 2017-02-24 13:44:54
does it exist?
