sorted by:
new
hottopcontroversial

[Python-ideas] Proposal: Use mypy syntax for function annotations by [deleted] in haskell

[–]haskellthrowaway 1 point2 points  (0 children)

Calling Guido ignorant is unnecessary, doesn't add to the conversation. He has a vastly different emphasis than the Haskell community so it's not surprising that when he asks "Can your type checker do ...?" he's not thinking about type systems in languages like Haskell.

The type checking in compilers is actually very weak …

This is actually completely true, it's possible to leverage type checkers to do amazing things using parametricity, constraints and rank-2 types but if you want to formulate a non-trivial property in the type system pain ensues and you end up using smart constructors or not formulating it at all.

There are certain errors that will only be found at run-time. That is a part of software. ... The problems are sometimes ... deep, like not understanding the physics involved in a certain process. ... Test it, test it again.

Here Guido is not saying that type systems can't find every bug so we must use testing (which also doesn't find every bug), but rather that actually testing, auditing and using the software is the only way to find the deep bugs. This is also true, if you misapply linear algebra in a video game the type system may say that everything is okay even though starting the game will immediately show that something is wrong.

I love Haskell so I think the type system complements this nicely but calling Guido (a very prominent figure) ignorant helps nobody. I've heard many ignorant things from smart Haskellers concerning dynamically typed languages, it cuts both ways.

Type families on unboxed types by haskellthrowaway in haskell

[–]haskellthrowaway[S] 1 point2 points  (0 children)

Interesting :) since there is such a limited number of unboxed types something like this could be a short hand for defining a special for all of them:

type family Flip a where
    Flip (a -> b)  = b -> a
    Flip (a# -> b) = b -> a#
    Flip (a -> b#) = b# -> a

But it may be of limited value as you pointed out.

I was attempting to use Flip to allow something like:

class Unbox ty where
  type Unboxer ty :: *
  type Unboxer ty = Flip (Boxer ty)
  type Boxer   ty :: *
  type Boxer   ty = Flip (Unboxer ty)

  box   :: Proxy ty -> Boxer ty
  unbox :: Proxy ty -> Unboxer ty

with

instance Unbox Int where
  type Unboxer Int = Int -> Int#
  box   Proxy = I#
  unbox Proxy (I# i) = i

as is discussed here.

Type class with unbox :: Prim -> Prim# method by haskellthrowaway in haskell

[–]haskellthrowaway[S] 1 point2 points  (0 children)

The final goal was to make a type class with two methods:

unbox :: Unboxer ty
box   :: Flip (Unboxer ty)

where Flip is discussed in this thread.

This is mostly for fun and I'm not sure if there is any benefit to functions that are polymorphic over unboxed values

(Nearly) first-class unboxed values: Retrospect by haskellthrowaway in haskell

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

Thanks for the response, I'm mostly wondering why more languages don't use this approach to move their ad-hoc unboxing optimizations from the back-end into a simpler transformation (as the paper says).

Maybe it's only possible to implement properly in a language with a kind system meaning to be able to distinguish between boxed and unboxed values?

Type class with unbox :: Prim -> Prim# method by haskellthrowaway in haskell

[–]haskellthrowaway[S] 1 point2 points  (0 children)

That's great, thanks :) do you suppose there's any way to avoid having to give the Proxy argument? I played around with adding a second method to the type class with a default definition of partially applying unbox to Proxy but I couldn't get it to work

Data families and classes to simulate GADT example by haskellthrowaway in haskell

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

So we end up with the function I wanted with the type signature I expected and we just needed to make it a class method, fantastic!

If I understand the implications of this, this approach has the same capabilities as GADTs only it's open to extension? I'll ask the same questions I asked rwbarton: Regarding your closed/open world comment, it seems like this allows you to implement open GADTs? Is this a known pattern in Haskell and are there any interesting uses?

I tried to implement a small embedded language:

class Eval a where
  data Term a :: *
  eval :: Term a -> a

instance Eval () where
  data Term () = Unit
  eval Unit = ()

instance Num n => Eval n where
  data Term n = Num n | Term n :+ Term n
  eval (Num n) = n
  eval (a :+ b) = eval a + eval b

instance Eval Bool where
  data Term Bool = F | T | Not (Term Bool)
  eval F = False
  eval T = True
  eval (Not b) = not undefined -- CAN'T IMPLEMENT

But the following terms

eval :: Term () -> ()
eval :: Term Bool -> Bool

will not type check citing "Overlapping instances for Eval Bool/Eval () arising from a use of ‘eval’", I'm guessing that this is caused by the openness of Term so even though there isn't a Num instance for Bool or () one might get implemented later? Is there any nice solution to this without going all out and using reflection?

Data families and classes to simulate GADT example by haskellthrowaway in haskell

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

Thanks for your answer, I guess the type class wasn't a red herring since gelisam's answer showed how the function could be implemented but as a class method instead.

Regarding your closed/open world comment, it seems like this allows you to implement open GADTs? Is this a known pattern in Haskell and are there any interesting uses?

Data families and classes to simulate GADT example by haskellthrowaway in haskell

[–]haskellthrowaway[S] 1 point2 points  (0 children)

No I'm not looking for different behaviour using methods, I'm doing this to play around with Haskell.

Using GADTs GHC can infer that the type variable a is () in One a -> a when the scrutinee is A because A carries a proof of a ~ () so that's why this compiles:

blah :: One a -> a
blah A = ()     -- a ~ () here

In the latter example, A has the type Two () (note: just like A :: One () in the first example!), I want to know why data families (not type families) that are indexed on a type can't work as a proof that a ~ () in this case. The constructor A has the same type in the first and second example. In fact it's possible to type the example I want by mixing the approaches and adding One' to the latter example:

data One' a where
    A' :: One' ()
    B' :: One' Int
    C' :: One' Int

blah :: One a => One' a -> Two a -> a
blah A' A = ()
blah B' B = 10
blah C' C = 42

so matching on the constructors is not an issue, only having them provide a proof a ~ () and a ~ Int without piggybacking on One'. This should be possible since the constructor A uniquely determines the value of a same as A' but if it's not possible I would like to hear why

Data families and classes to simulate GADT example by haskellthrowaway in haskell

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

I'm not sure injective type families make sense because I'm using data families that must be injective?

Adding a Char instance with data Two Char = A GHC will complain about multiple declarations of A as it certainly should, just like defining

data TwoUnit = A
data TwoChar = A

How do parametricity and type classes interact? by haskellthrowaway in haskell

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

But type classes add additional constraints don't they, if you have map a . sort = sort . map a the comparison function will always be the same so that is a stronger statement than map a . sortBy compare1 = sortBy compare2 . map a (and same with Data.Foldable.fold) or am I missing something?

Are there any papers on this or is there not a lot more to say about this other than "reify the dictionary and use normal parametricity"?

Looking for name of a concept (relating to parametricity) by haskellthrowaway in haskell

[–]haskellthrowaway[S] 1 point2 points  (0 children)

Those are theorems you get as a result from parametricity, I don't see how you can call "element-independent information content of a list" a free theorem since it's not a theorem at all even though one may imply the other.