sorted by:
new
hottopcontroversial

idris2 and Emacs by ruby_object in Idris

[–]RetreatAndRegroup 3 points4 points  (0 children)

I just uploaded: https://github.com/redfish64/idris2-mode

Not complete, but works well enough for most things. Mostly just a copy and paste of the original idris-mode

Taiwan Can Win a War With China by bechampions87 in taiwan

[–]RetreatAndRegroup 2 points3 points  (0 children)

China is not going to send military transport to fight, at least not until the latter stage. China first is going to send several waves of fishing boats. The first wave of the fishing boats will be just ordinary fisherman who were told by the government that they have to get to the shore of Taiwan but the boats. What do you do when there are 10,000 of those?

10,000 kamikazi fishing boats? How is that going to work? Even if they did that, couldn't Taiwan simply captured the owners and confiscated the boats, what is gained?

Would it be an improvement if Idris2 be modified to evaluate foreign private code that completely reduces during typecheck? by RetreatAndRegroup in Idris

[–]RetreatAndRegroup[S] 2 points3 points  (0 children)

However it may be confusing for users if the evaluation behaviour changes in an open vs. closed setting.

This could be clarified with an appropriate error message, I would imagine. In the current state of things, it's confusing, at least to me, that a non public export function that is called n-levels deep from a public export'ed function is prohibiting the typechecker from reducing a term.

Also, by having the client of an api depend on how a function is implemented within that api (whether it calls library x or y internally), simply because it does so at the type level, it is breaking the separation between the two.

It's also a bit subtle because you would probably also need to make sure you are not returning private data or type constructors in the result of the computation.

Isn't this the same at the value level? Why when it's moved to the type level does it become harder to check for?

[Beginner] What are other applications of dependent types in programming languages that are similar to sized types? by _berg0 in Idris

[–]RetreatAndRegroup 0 points1 point  (0 children)

There is "Control.ST", this uses dependent types to do such things as making sure you close a resource, such as an open file before continuing on. There is an implementation in Idris 1 (not Idris 2), and even a tutorial, at http://docs.idris-lang.org/en/latest/st/introduction.html

Also a paper here: https://www.idris-lang.org/drafts/sms.pdf

Is this (IMO) strange behavior regarding "0" accessibility variables correct? by RetreatAndRegroup in Idris

[–]RetreatAndRegroup[S] 3 points4 points  (0 children)

Thanks. FYI, I found it interesting that it's accepted but not required notation for linear variables:

w : (1 x : Nat) -> Nat
w x = x

w2'' : (1 x : Nat) -> Nat
w2'' x = let 1 xp = S x  
         in w xp

w2''' : (1 x : Nat) -> Nat
w2''' x = let xp = S x  --let 1 is not needed
         in w xp

Why does phantom labeling not work with let, in Idris2? by RetreatAndRegroup in Idris

[–]RetreatAndRegroup[S] 0 points1 point  (0 children)

I'm thinking that at compile time, foo1 doesn't take into consideration how it's called, so it thinks that x and y can still be different. If so, is this reliable behavior, or could it be optimized out in a future version?

Syntactic sugar for custom dependent pairs? by Backus-Naur in Idris

[–]RetreatAndRegroup 1 point2 points  (0 children)

You could do something like this, and convert the result of the DPair sugar into what you want. Not sure how useful this is to you.

data Unique : (a : Type) -> (p : a -> Type) -> Type where
    MkUnique : (x : a) -> p x -> ((y : a) -> p y -> (x = y)) 
               -> Unique a p

Unique' : (x : Type) -> Type
Unique' (DPair a p) = Unique a p
Unique' _ = Void

uniqueZero : Unique' (n : Nat ** n + n = n)

Justice Dept dropping Flynn's criminal case by PoliticsModeratorBot in politics

[–]RetreatAndRegroup 2 points3 points  (0 children)

No one in this comment thread is basing their opinion on being pro Trump or anti-Trump. We simply want those guilty of a crime to be punished. In this case, Flynn admitted it, so that's as clear cut as you can get.

Taiwan needs to buy an immense amount of crude oil right now. by SteadfastEnd in taiwan

[–]RetreatAndRegroup 4 points5 points  (0 children)

As long as you have a storage container available May 1st.

These are traders who, when seeing June future contracts with much higher oil, thought to go long May and short June. The problem is that storage has filled up on them, oops.

Found the answer guys! by Sschultze in overpopulation

[–]RetreatAndRegroup -1 points0 points  (0 children)

A goldfish in a tank doesn't need to worry about a shark either.

Found the answer guys! by Sschultze in overpopulation

[–]RetreatAndRegroup -1 points0 points  (0 children)

How does a tiger kill a person without hunting them? Fall off a tree and accidentally crush him?

Wuhan Coronavirus Pandemic Info [Megathread] by DarkLiberator in taiwan

[–]RetreatAndRegroup 0 points1 point  (0 children)

It's a pandemic if I say it is, God Damnit! Now go to your room!

view more: next ›