Changes between Version 3 and Version 4 of NewtypeWrappers


Ignore:
Timestamp:
Jan 15, 2013 11:20:46 AM (2 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