Changes between Version 3 and Version 4 of NewtypeWrappers


Ignore:
Timestamp:
Jan 15, 2013 11:20:46 AM (3 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewtypeWrappers

    v3 v4  
    4141 * For `x3`, we'd have to map over `T`, thus `mapT MkAge x3`.  But what if `mapT` didn't exist?  We'd have to make it. And not all data types have maps. `S` is a harder one: you could only map over S-values if `m` was a functor.  There's a lot of discussion abou this on #2110.
    4242
    43 == The proposal ==
     43== The opportunity ==
    4444
    4545Clearly what we want is a way to "lift" newtype constructors (and dually deconstructors)
     
    6464}}}
    6565
    66 So all we need is concrete syntax to allow you to ask for these lifed coercions in Haskell.  I couldn't think of a good way to do this, but now I have a proposal:
     66So all we need is concrete syntax to allow you to ask for these lifed coercions in Haskell. 
     67
     68== Proposal 1 ==
     69
     70The first possiblity involves a new top-level declaration:
    6771{{{
    6872  newtype wrap w1 :: [Int] -> [Age])
     
    97101  newtype wrap foo :: (Int -> Int) -> Fun Age
    98102}}}
     103
     104== Proposal 2 ==
     105
     106The second possibility is superficially simpler: just provided a new built-in constant with type
     107{{{
     108  newtypeCast :: NTC a b => a -> b
     109}}}
     110Here `NTC` is a built-in type class that witnesses the (free) conversion between `a` and `b`.  Although it would not quite be implemented like this, we would have a built-in instance for each data type (but see Type Soundness below):
     111{{{
     112  instance NTC a b => NTC [a] [b]
     113}}}
     114and two built-in instances for each newtype:
     115{{{
     116  instance NTC Int b => NTC Age b
     117  instance NTC a Int => NTC a Age
     118}}}
     119So to solve a `NTC` constraint you unwwap all those newtypes (being careful about abstraction; see next section). 
     120
     121This plan requires a bit more paddling under the water on GHC's part, especially during type inference, but it looks a lot more straightforward than I first thought.  Thanks to Roman Cheplyka for advocating this solution.
    99122
    100123== Abstraction ==
     
    139162         data Map a b = MkMap (InternalMap a b)
    140163}}}
    141   it's no good being able to see the data constructor `MkMap`; you need to
     164  It's no good just being able to see the data constructor `MkMap`; you need to
    142165  see the constructors of `InternalMap` too.
    143166
     
    165188}}}
    166189The problem is, as usual, the type function hiding inside T's definition.
    167 The solution is described in [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
    168 Generative type abstraction and type-level computation].  It is still not implemented, alas,
     190The solution is described in [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/ Generative type abstraction and type-level computation].  It is still not implemented, alas,
    169191but adding the newtype wrappers introduces no problems that we do not already have.
    170192