Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion
Hi Adam, On 6 Feb 2015, at 21:31, Adam Gundry a...@well-typed.com wrote: What does all monomorphic cases mean? Is the idea what GHC would typecheck an expression involving a literal integer, determine that the occurrence had type Even, then evaluate the TH splice *after* typechecking? Whereas if the occurrence had a non-ground type, it would do something else? Yes, Typed TH already runs *after* type checking, which is what allows you to do validation based on the resulting type. The main reason why I was only proposing to do this for monomorphic values is, because, how could you possible validate a polymorphic literal? Which validation function would you use? You could ban polymorphic literals, but that'd involve eliminating most uses of polymorphic Num functions (as I mentioned as another email), which would break so much code it would render the extension unusable in real code. I'm open to better ideas on how to tackle this, the main reason I started this discussion is because I don't really like this polymorphic literals fail at compile time thing either. I just don't see how to solve it without going all dependent types on the problem. None of this is particularly persuasive, I'm afraid. Is it worthwhile introducing something new just to avoid having to write a quasi quote? Actually, I would be mildly ok with quasi quoters, BUT there currently is no Typed TH quasi quoter (as mentioned on the wiki page), additionally, such a quoter does not have access to Lift instances for all but a handful of datatypes until we have a more comprehensive way to generate Lift instances. I think both of these points are also highly relevant for this dicussion. I *am* attracted to the idea of indexed classes in place of IsString/Num class KnownSymbol s = IsIndexedString (a :: *) (s :: Symbol) where fromIndexedString :: a class KnownInteger i = IsIndexedInteger (a :: *) (i :: Integer) where fromIndexedInteger :: a These have a smooth upgrade path from the existing class instances via default fromIndexedString :: (KnownSymbol s, IsString a) = a fromIndexedString = fromString (symbolVal (Proxy :: Proxy s)) default fromIndexedInteger :: (KnownInteger i, Num a) = a fromIndexedInteger = fromInteger (integerVal (Proxy :: Proxy i)) and other instances can take advantage of the additional type information. perhaps we need to bring Dependent Haskell a bit closer before this is justifiable... The main reason I don't like the dependent haskell approach or your approach is how much boiler plate it introduces for beginners. ANYONE knows how to write a String - Maybe a function, I barely know how to use your example and I'm very comfortable with the type families/datakinds stuff, how would ordinary haskellers use that? Not to mention, how would I use your IsIndexedString in real code? It seems you'd need at least a FunDep + cumbersome annotation? Not to mention that it still performs the conversion at runtime (I would *much* rather have a Lift based approach that just splices finished conversions into the resulting program. Cheers, Merijn signature.asc Description: Message signed with OpenPGP using GPGMail ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion
Hi Merijn, Thanks for persevering with explaining things to me. :-) On 09/02/15 09:47, Merijn Verstraaten wrote: On 6 Feb 2015, at 21:31, Adam Gundry a...@well-typed.com wrote: What does all monomorphic cases mean? Is the idea what GHC would typecheck an expression involving a literal integer, determine that the occurrence had type Even, then evaluate the TH splice *after* typechecking? Whereas if the occurrence had a non-ground type, it would do something else? Yes, Typed TH already runs *after* type checking, which is what allows you to do validation based on the resulting type. The main reason why I was only proposing to do this for monomorphic values is, because, how could you possible validate a polymorphic literal? Which validation function would you use? You could ban polymorphic literals, but that'd involve eliminating most uses of polymorphic Num functions (as I mentioned as another email), which would break so much code it would render the extension unusable in real code. I'm open to better ideas on how to tackle this, the main reason I started this discussion is because I don't really like this polymorphic literals fail at compile time thing either. I just don't see how to solve it without going all dependent types on the problem. In the absence of a coherent story for polymorphism, I think the right thing to do is to be able to specify a particular validator, rather than try to have type inference determine a monomorphic type and otherwise get stuck... None of this is particularly persuasive, I'm afraid. Is it worthwhile introducing something new just to avoid having to write a quasi quote? Actually, I would be mildly ok with quasi quoters, BUT there currently is no Typed TH quasi quoter (as mentioned on the wiki page), additionally, such a quoter does not have access to Lift instances for all but a handful of datatypes until we have a more comprehensive way to generate Lift instances. I think both of these points are also highly relevant for this dicussion. ...so is the right solution to introduce Typed TH quasiquoters for expressions? Sorry, I presumed such a thing existed, as Typed TH is rather regrettably underdocumented. Is there any particular difficulty with them, or is it just a Small Matter of Programming? I think the lack of Lift instances is a separate problem; while it looks like 7.10 will be better in this respect and dataToExpQ goes a fair way, I agree that making them easier to generate would be nice. Perhaps a generics-based default method combined with DeriveAnyClass would make deriving Lift possible? Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/ ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Injective type families for GHC
Haskellers, I am finishing work on adding injective type families to GHC. I know that in the past many people have asked for this feature. If you have use cases for injective type families I would appreciate if you could show them to me. My implementation has some restrictions and I want to see how severe these restrictions are from a practical point of view. Janek --- Politechnika Łódzka Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] Injective type families for GHC
Hi Jan,
One example is https://github.com/haskell/vector/issues/34
I see lots of potential uses in HList. For example in HZip.hs there's
a Zip using type families:
type family HZipR (x::[*]) (y::[*]) :: [*]
type instance HZipR '[] '[] = '[]
type instance HZipR (x ': xs) (y ': ys) = (x,y) ': HZipR xs ys
If there was no need to write some additional type families that tell
ghc how to find x and y given HZipR x y, then the version using TFs
might be as good as the version using FDs (defined in HList.hs)
I don't know how realistic this is but a constraint (HLength x ~
HLength y) would ideally have the same result as SameLength x y.
Copy-paste into ghci:
:set +t -XDataKinds -XFlexibleContexts -XTypeFamilies
import Data.HList
let desired = Proxy :: SameLength x '[(),()] = Proxy x
let current = Proxy :: (HLength y ~ HLength '[(),()]) = Proxy y
Prints
desired :: Proxy '[y, y1]
current :: HLength y ~ 'HSucc ('HSucc 'HZero) = Proxy y
Regards,
Adam
On Mon, Feb 9, 2015 at 10:58 AM, Jan Stolarek jan.stola...@p.lodz.pl wrote:
Haskellers,
I am finishing work on adding injective type families to GHC. I know that in
the past many people
have asked for this feature. If you have use cases for injective type
families I would appreciate
if you could show them to me. My implementation has some restrictions and I
want to see how
severe these restrictions are from a practical point of view.
Janek
---
Politechnika Łódzka
Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata.
Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez
pomyłkę
prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie.
___
Haskell-Cafe mailing list
haskell-c...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ANNOUNCE: GHC 7.10.1 Release Candidate 2
On 27 January 2015 at 01:13, Austin Seipp aus...@well-typed.com wrote: We are pleased to announce the second release candidate for GHC 7.10.1: Thanks, I updated my Fedora ghc-7.10 Copr repo to RC2: https://copr.fedoraproject.org/coprs/petersen/ghc-7.10/ (The build is currently only for Rawhide but I think it should work on Fedora 21 too.) Jens ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
