Re: [Haskell-cafe] Help to write type-level function
I think it might be impossible with type families. I don't think it's possible to differentiate with type families something like T a a, and T a b, with b different from a. I think that you would need overlap to write this. Here'shttp://www.haskell.org/ghc/docs/7.4.2/html/users_guide/type-families.html#data-family-overlapthe GHC page on it. With type families you can do overlap, but in that case, the result of unification must be the same. So basically : T a a === T a b (with b set to a) whereas the intuitive way of doing Find requires a way of differentiating between these two cases. On Wed, Feb 27, 2013 at 4:33 PM, Dmitry Kulagin dmitry.kula...@gmail.comwrote: Hi, I try to implement typed C-like structures in my little dsl. I was able to express structures using type-level naturals (type Ty is promoted): data Ty = TInt | TBool | TStruct Symbol [Ty] That allowed to implement all needed functions, including type-level function: type family Get (n :: Nat) (xs :: [Ty]) :: Ty But it is not very convenient to identify struct's fields using naturals, and I wanted to change Ty definition to: data Ty = TInt | TBool | TStruct Symbol [(Symbol, Ty)] It is much closer to how C-struct looks, but I was unable to implement required type function: type family Find (s :: Symbol) (xs :: [(Symbol,Ty)]) :: Ty Which just finds a type in a associative list. Could someone give me a hint, how to do it? Or perhaps, is it just impossible thing to do? Thanks! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Help to write type-level function
On 27 February 2013 12:01, Raphael Gaschignard dasur...@gmail.com wrote: I think it might be impossible with type families. I don't think it's possible to differentiate with type families something like T a a, and T a b, with b different from a. It's indeed impossible to write such type function using type families. It will be possible with new closed type familes (they are in GHC head already). But for now it's possible to use overlapping instances and fundeps. Implementation of type level equality is simple and it's only instances which need ovelap. -- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b - eq instance TypeEq a a True instance eq ~ False = TypeEq a b eq Implementation of lookup by key is relatively straightforward. Note that it doesn't check that key is unique. data k : v infix 6 : -- | Lookup type for given key class TyLookup (map :: [*]) (k :: *) (v :: *) | map k - v where class TyLookupCase (map :: [*]) (k :: *) (v :: *) (eq :: Bool) | map k eq - v where instance ( TypeEq k k' eq , TyLookupCase (k : v ': xs) k' v' eq ) = TyLookup (k : v ': xs) k' v' where instance TyLookupCase (k : v ': xs) k v True where instance TyLookup xs k v = TyLookupCase (k' : v' ': xs) k v False where ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Help to write type-level function
Dmitry Kulagin wrote: I try to implement typed C-like structures in my little dsl. HList essentially had those http://code.haskell.org/HList/ I was unable to implement required type function: type family Find (s :: Symbol) (xs :: [(Symbol,Ty)]) :: Ty Which just finds a type in a associative list. HList also implemented records with named fields. Indeed, you need a type-level lookup in an associative list, and for that you need type equality. (The ordinary List.lookup has the Eq constraint, doesn't it?) Type equality can be implemented with type functions, right now. http://okmij.org/ftp/Haskell/typeEQ.html#TTypeable (That page also defined a type-level list membership function). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Help to write type-level function
That seems to be very relevant to my problem (especially HList.Record). Am I right that UndecidableInstances is required mostly because of eq on types, like in this instances: class HRLabelSet (ps :: [*]) instance HRLabelSet '[] instance HRLabelSet '[x] instance ( HEq l1 l2 leq , HRLabelSet' l1 l2 leq r ) = HRLabelSet (LVPair l1 v1 ': LVPair l2 v2 ': r) so the usage of the extension is unavoidable for my purposes? Thank you! On Wed, Feb 27, 2013 at 12:28 PM, o...@okmij.org wrote: Dmitry Kulagin wrote: I try to implement typed C-like structures in my little dsl. HList essentially had those http://code.haskell.org/HList/ I was unable to implement required type function: type family Find (s :: Symbol) (xs :: [(Symbol,Ty)]) :: Ty Which just finds a type in a associative list. HList also implemented records with named fields. Indeed, you need a type-level lookup in an associative list, and for that you need type equality. (The ordinary List.lookup has the Eq constraint, doesn't it?) Type equality can be implemented with type functions, right now. http://okmij.org/ftp/Haskell/typeEQ.html#TTypeable (That page also defined a type-level list membership function). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Help to write type-level function
Very clear solution, I will try to adopt it. Thank you! On Wed, Feb 27, 2013 at 12:17 PM, Aleksey Khudyakov alexey.sklad...@gmail.com wrote: On 27 February 2013 12:01, Raphael Gaschignard dasur...@gmail.com wrote: I think it might be impossible with type families. I don't think it's possible to differentiate with type families something like T a a, and T a b, with b different from a. It's indeed impossible to write such type function using type families. It will be possible with new closed type familes (they are in GHC head already). But for now it's possible to use overlapping instances and fundeps. Implementation of type level equality is simple and it's only instances which need ovelap. -- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b - eq instance TypeEq a a True instance eq ~ False = TypeEq a b eq Implementation of lookup by key is relatively straightforward. Note that it doesn't check that key is unique. data k : v infix 6 : -- | Lookup type for given key class TyLookup (map :: [*]) (k :: *) (v :: *) | map k - v where class TyLookupCase (map :: [*]) (k :: *) (v :: *) (eq :: Bool) | map k eq - v where instance ( TypeEq k k' eq , TyLookupCase (k : v ': xs) k' v' eq ) = TyLookup (k : v ': xs) k' v' where instance TyLookupCase (k : v ': xs) k v True where instance TyLookup xs k v = TyLookupCase (k' : v' ': xs) k v False where ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Help to write type-level function
Hi Aleksey, Unfortunately, your solution does not work for me (ghc 7.6.2). I reduced the problem to: -- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b - eq instance TypeEq a a True -- instance TypeEq a b False instance eq ~ False = TypeEq a b eq f :: TypeEq Int Int True = Int f = 1 When I try to invoke f, I get overlapping instances error: Overlapping instances for TypeEq * Int Int 'True arising from a use of `f' Matching instances: instance TypeEq k a a 'True -- Defined at Test.hs:14:24 instance eq ~ 'False = TypeEq k a b eq -- Defined at Test.hs:16:10 Thanks. On Wed, Feb 27, 2013 at 12:17 PM, Aleksey Khudyakov alexey.sklad...@gmail.com wrote: On 27 February 2013 12:01, Raphael Gaschignard dasur...@gmail.com wrote: I think it might be impossible with type families. I don't think it's possible to differentiate with type families something like T a a, and T a b, with b different from a. It's indeed impossible to write such type function using type families. It will be possible with new closed type familes (they are in GHC head already). But for now it's possible to use overlapping instances and fundeps. Implementation of type level equality is simple and it's only instances which need ovelap. -- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b - eq instance TypeEq a a True instance eq ~ False = TypeEq a b eq Implementation of lookup by key is relatively straightforward. Note that it doesn't check that key is unique. data k : v infix 6 : -- | Lookup type for given key class TyLookup (map :: [*]) (k :: *) (v :: *) | map k - v where class TyLookupCase (map :: [*]) (k :: *) (v :: *) (eq :: Bool) | map k eq - v where instance ( TypeEq k k' eq , TyLookupCase (k : v ': xs) k' v' eq ) = TyLookup (k : v ': xs) k' v' where instance TyLookupCase (k : v ': xs) k v True where instance TyLookup xs k v = TyLookupCase (k' : v' ': xs) k v False where ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Help to write type-level function
On 27.02.2013 17:35, Dmitry Kulagin wrote:
Hi Aleksey,
Unfortunately, your solution does not work for me (ghc 7.6.2). I reduced
the problem to:
-- | Type class for type equality.
class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b - eq
instance TypeEq a a True
-- instance TypeEq a b False
instance eq ~ False = TypeEq a b eq
You need to add pragma {-# LANGUAGE OverlappingInstances #-}
to the file where instances defined. Without it GHC will complain
about overlap and unlike other extensions won't recommend pragma
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Help to write type-level function
Oh, that is my fault - I was sure that I specified the extension and it
didn't help.
It really works with OverlappingUndecidable.
Thank you!
On Wed, Feb 27, 2013 at 10:36 PM, Aleksey Khudyakov
alexey.sklad...@gmail.com wrote:
On 27.02.2013 17:35, Dmitry Kulagin wrote:
Hi Aleksey,
Unfortunately, your solution does not work for me (ghc 7.6.2). I reduced
the problem to:
-- | Type class for type equality.
class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b - eq
instance TypeEq a a True
-- instance TypeEq a b False
instance eq ~ False = TypeEq a b eq
You need to add pragma {-# LANGUAGE OverlappingInstances #-}
to the file where instances defined. Without it GHC will complain
about overlap and unlike other extensions won't recommend pragma
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Help to write type-level function
Hi, I try to implement typed C-like structures in my little dsl. I was able to express structures using type-level naturals (type Ty is promoted): data Ty = TInt | TBool | TStruct Symbol [Ty] That allowed to implement all needed functions, including type-level function: type family Get (n :: Nat) (xs :: [Ty]) :: Ty But it is not very convenient to identify struct's fields using naturals, and I wanted to change Ty definition to: data Ty = TInt | TBool | TStruct Symbol [(Symbol, Ty)] It is much closer to how C-struct looks, but I was unable to implement required type function: type family Find (s :: Symbol) (xs :: [(Symbol,Ty)]) :: Ty Which just finds a type in a associative list. Could someone give me a hint, how to do it? Or perhaps, is it just impossible thing to do? Thanks! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
