benzrf 2017-02-04 13:47:15
inductive definitions vs propositional definitions?
benzrf 2017-02-04 13:47:18
whats the distinction
erisco 2017-02-04 13:49:10
for example you can use Fin n or you can use (Z :<= x) ~ 'True, (x :< n) ~ 'True
erisco 2017-02-04 13:49:54
Fin defines how to construct all the naturals in the finite range whereas the proposition says what is true about naturals in the range
benzrf 2017-02-04 13:51:19
ah
erisco 2017-02-04 13:52:12
or in use it is the difference between showing how to construct the natural and showing that your natural satisfies the proposition
raynold 2017-02-04 13:52:17
ahh it's a wonderful day
erisco 2017-02-04 13:56:52
raynold, night, but who's looking
TRManderson 2017-02-04 13:57:37
Anyone here run into -fPIC issues on Ubuntu 16.04?
TRManderson 2017-02-04 13:58:03
I can compile plain Haskell fine, I'm just struggling to get the shared object I'm trying to export to compile without linker errors
TRManderson 2017-02-04 13:59:45
I've tried it with stack-installed GHC 7 and 8, and nix-installed GHC 8
jle` 2017-02-04 14:00:39
erisco: i think you can exploit the structure when using it so it's a lot simpler in certain use cases
jle` 2017-02-04 14:00:47
but, there's probably a lot similar
jle` 2017-02-04 14:01:11
in your type, your proofs will be at the whim of the :<= / :< type families
jle` 2017-02-04 14:01:27
for Fin, the proofs don't have to worry about the type families, they're just directly structural
erisco 2017-02-04 14:01:54
yes
jle` 2017-02-04 14:02:03
but ultimately if the :<= type family is defined inductively, then a lot of the overal sturcture of your proofs will be the same. just a difference in syntax and implementation
erisco 2017-02-04 14:02:24
is there something in Idris which corresponds to the type family approach of :<= and :< ? I've only seen inductive
jle` 2017-02-04 14:03:06
well you can do definitional equality in idris too
erisco 2017-02-04 14:03:09
well I only looked under the hood so far, not sure where the bottom in
jle` 2017-02-04 14:03:14
<= and < will be just normal functions
jle` 2017-02-04 14:03:19
and you can use them at the type level
EvanR 2017-02-04 14:03:30
if its a type family, that would correspond to a ... type family, that is a function of type MyIndex -> Type
jle` 2017-02-04 14:03:42
in idris you'd define <= and < for normal nat's, and then you can use them for type level nats too
jle` 2017-02-04 14:03:47
because type level nats are just normal nats
erisco 2017-02-04 14:03:58
EvanR, I suppose so :)
EvanR 2017-02-04 14:04:13
if it really should be a regular value function, but cant be in haskell, then it should be a regular value function in idris
EvanR 2017-02-04 14:04:35
nat arithmetic has no crazy type level shenanigans in idris
erisco 2017-02-04 14:04:42
well I'd expect something like Leq instead of :<=
EvanR 2017-02-04 14:04:49
its called LTE
erisco 2017-02-04 14:04:53
but then if you want theorems isn't that were :<= comes in?
jle` 2017-02-04 14:05:04
so you'd have Bounded :: (Z <= x = True) -> (x < n == True) -> x -> Bounded n
jle` 2017-02-04 14:05:13
s/==/=
EvanR 2017-02-04 14:05:29
LTEZero : LTE 0 right, LTESucc : LTE left right -> LTE (S left) (S right)
erisco 2017-02-04 14:05:35
or maybe not, I guess you'd just say Leq a b -> Leq a (S b) and so on
jle` 2017-02-04 14:05:48
but even better would be Bounded :: (Z <= x) -> (x < n) -> x -> Bounded n
jle` 2017-02-04 14:06:00
instead of definitional equality (~ True)
jle` 2017-02-04 14:06:12
you'd have actual witnesses for LTE/LE
EvanR 2017-02-04 14:06:17
MkBetween : LTE a n -> LTE b n -> Between a b n
jle` 2017-02-04 14:06:18
which is what that one module you showed me had
jle` 2017-02-04 14:06:34
but in the end, the two types are sort of the same
jle` 2017-02-04 14:06:57
constructing a witness for (x, x < n), and constructing a Fin n, would be more or less the same
jle` 2017-02-04 14:06:59
you'd do them both inductively
EvanR 2017-02-04 14:07:11
instead of separate types for numbers that are within a range or non-zero, you can just have extra predicates defined on numbers
EvanR 2017-02-04 14:07:24
even, prime, whatever
EvanR 2017-02-04 14:07:44
then you only have to implement arithmetic once
EvanR 2017-02-04 14:08:03
Fin on the other hand doesnt have arithmetic, youd use it for a set of finite indices
EvanR 2017-02-04 14:08:19
it serves the same role as finite sets
EvanR 2017-02-04 14:08:22
rather than numbers
erisco 2017-02-04 14:08:27
jle`, well it seems to me like we could do that in Haskell with Leq and a Lneq
jle` 2017-02-04 14:08:37
yeah, it's the same thing
jle` 2017-02-04 14:08:41
from that module you showed, http://hackage.haskell.org/package/type-natural-0.7.1.2/docs/Data-Type-Natural.html#t:Leq
jle` 2017-02-04 14:09:19
`exists x. Leq x n` and `Fin n` should be structurally the same
jle` 2017-02-04 14:09:31
*Lneq, but yeah
jle` 2017-02-04 14:10:17
(your BoundedAbove type could have also been exists x. Lneq x n, yeah)
jle` 2017-02-04 14:10:39
all different ways of saying the same thing, neat right
jle` 2017-02-04 14:10:51
the '~ True' way would probably be my least favorite, heh
jle` 2017-02-04 14:11:25
that is, ~ True + type family. but i think working with all of them should be the same
EvanR 2017-02-04 14:11:32
Bools suck!
erisco 2017-02-04 14:11:34
but then what about the runtime considerations
jle` 2017-02-04 14:11:46
er, i mean, the same "proof tree"/proof structure. different mechanics of working with them
jle` 2017-02-04 14:11:52
time to benchmark :o
erisco 2017-02-04 14:11:55
yes, ~ 'True feels a lot like == True
EvanR 2017-02-04 14:12:00
erisco: ideally proofs dont happen at runtime?
EvanR 2017-02-04 14:12:18
types only exist at compile time
erisco 2017-02-04 14:12:20
yes but if we're carrying witnesses around in our data that means something
jle` 2017-02-04 14:12:25
haskell carries around most proofs like this at runtime
jle` 2017-02-04 14:12:29
idris erases a lot of them
EvanR 2017-02-04 14:12:29
gross
jle` 2017-02-04 14:12:44
the proofs have to be carried because in general, types are erased
jle` 2017-02-04 14:12:50
so the proofs act as witnesses to the types and their properties
jle` 2017-02-04 14:13:03
that 'in general' should have been at the beginning of the sentence
EvanR 2017-02-04 14:13:23
conceptually, you proved what you need to prove, and the code can run unchecked
EvanR 2017-02-04 14:13:38
but i know in haskell you use typeclasses to convert types to values at runtime
erisco 2017-02-04 14:14:30
hm, well I just don't know enough about the compiler and runtime
erisco 2017-02-04 14:14:42
it is similar to the newtype vs data options yesterday
spitfireee 2017-02-04 14:21:06
win 5$ only for register guys! NO JOKE - > https://www.dailyrewards.com/?r=ref362870&s=7
Tuplanolla 2017-02-04 14:21:55
Too bad all the register guys are over at ##asm.
